theorem funceq2 (F _A1 _A2 B: set): $ _A1 == _A2 -> (func F _A1 B <-> func F _A2 B) $;
_A1 == _A2 -> _A1 == _A2
_A1 == _A2 -> (func F _A1 B <-> func F _A2 B)