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_homomorphism ) ) & ( for h being Function of UA,UA holds

( h in F2 iff h is_homomorphism ) ) implies F1 = F2 )

assume that

A3: for h being Function of UA,UA holds

( h in F1 iff h is_homomorphism ) and

A4: for h being Function of UA,UA holds

( h in F2 iff h is_homomorphism ) ; :: thesis: F1 = F2

A5: for f being Element of F2 holds f is Function of UA,UA ;

A6: F2 c= F1

F1 c= F2

( h in F1 iff h is_homomorphism ) ) & ( for h being Function of UA,UA holds

( h in F2 iff h is_homomorphism ) ) implies F1 = F2 )

assume that

A3: for h being Function of UA,UA holds

( h in F1 iff h is_homomorphism ) and

A4: for h being Function of UA,UA holds

( h in F2 iff h is_homomorphism ) ; :: thesis: F1 = F2

A5: for f being Element of F2 holds f is Function of UA,UA ;

A6: F2 c= F1

proof

A8:
for f being Element of F1 holds f is Function of UA,UA
;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F2 or q in F1 )

assume A7: q in F2 ; :: thesis: q in F1

then reconsider h1 = q as Function of UA,UA by A5;

h1 is_homomorphism by A4, A7;

hence q in F1 by A3; :: thesis: verum

end;assume A7: q in F2 ; :: thesis: q in F1

then reconsider h1 = q as Function of UA,UA by A5;

h1 is_homomorphism by A4, A7;

hence q in F1 by A3; :: thesis: verum

F1 c= F2

proof

hence
F1 = F2
by A6, XBOOLE_0:def 10; :: thesis: verum
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F1 or q in F2 )

assume A9: q in F1 ; :: thesis: q in F2

then reconsider h1 = q as Function of UA,UA by A8;

h1 is_homomorphism by A3, A9;

hence q in F2 by A4; :: thesis: verum

end;assume A9: q in F1 ; :: thesis: q in F2

then reconsider h1 = q as Function of UA,UA by A8;

h1 is_homomorphism by A3, A9;

hence q in F2 by A4; :: thesis: verum