let F1, F2 be FUNCTION_DOMAIN of the carrier of UA, the carrier of UA; :: thesis: ( ( for h being Function of UA,UA holds
( h in F1 iff h is_isomorphism UA,UA ) ) & ( for h being Function of UA,UA holds
( h in F2 iff h is_isomorphism UA,UA ) ) implies F1 = F2 )
assume that
A3: for h being Function of UA,UA holds
( h in F1 iff h is_isomorphism UA,UA ) and
A4: for h being Function of UA,UA holds
( h in F2 iff h is_isomorphism UA,UA ) ; :: thesis: F1 = F2
A5: F2 c= F1

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in F2 or q in F1 )
assume A6: q in F2 ; :: thesis: q in F1
then reconsider h1 = q as Function of UA,UA by FUNCT_2:def 12;
h1 is_isomorphism UA,UA by A4, A6;
hence q in F1 by A3; :: thesis: verum

end;

F1 c= F2

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in F1 or q in F2 )
assume A7: q in F1 ; :: thesis: q in F2
then reconsider h1 = q as Function of UA,UA by FUNCT_2:def 12;
h1 is_isomorphism UA,UA by A3, A7;
hence q in F2 by A4; :: thesis: verum

end;

hence F1 = F2 by A5, XBOOLE_0:def 10; :: thesis: verum