let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G; :: thesis: ( ( for f being Element of F1 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds

( h in F1 iff ( h is one-to-one & h is onto ) ) ) & ( for f being Element of F2 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds

( h in F2 iff ( h is one-to-one & h is onto ) ) ) implies F1 = F2 )

assume that

A4: for f being Element of F1 holds f is Homomorphism of G,G and

A5: for h being Homomorphism of G,G holds

( h in F1 iff ( h is one-to-one & h is onto ) ) and

A6: for f being Element of F2 holds f is Homomorphism of G,G and

A7: for h being Homomorphism of G,G holds

( h in F2 iff ( h is one-to-one & h is onto ) ) ; :: thesis: F1 = F2

A8: F2 c= F1

( h in F1 iff ( h is one-to-one & h is onto ) ) ) & ( for f being Element of F2 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds

( h in F2 iff ( h is one-to-one & h is onto ) ) ) implies F1 = F2 )

assume that

A4: for f being Element of F1 holds f is Homomorphism of G,G and

A5: for h being Homomorphism of G,G holds

( h in F1 iff ( h is one-to-one & h is onto ) ) and

A6: for f being Element of F2 holds f is Homomorphism of G,G and

A7: for h being Homomorphism of G,G holds

( h in F2 iff ( h is one-to-one & h is onto ) ) ; :: thesis: F1 = F2

A8: F2 c= F1

proof

F1 c= F2
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F2 or q in F1 )

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

then reconsider h1 = q as Homomorphism of G,G by A6;

( h1 is one-to-one & h1 is onto ) by A7, A9;

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

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

then reconsider h1 = q as Homomorphism of G,G by A6;

( h1 is one-to-one & h1 is onto ) by A7, A9;

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

proof

hence
F1 = F2
by A8, 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 A10: q in F1 ; :: thesis: q in F2

then reconsider h1 = q as Homomorphism of G,G by A4;

( h1 is one-to-one & h1 is onto ) by A5, A10;

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

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

then reconsider h1 = q as Homomorphism of G,G by A4;

( h1 is one-to-one & h1 is onto ) by A5, A10;

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