let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G; ( ( 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 ) )
; F1 = F2
A8:
F2 c= F1
F1 c= F2
hence
F1 = F2
by A8, XBOOLE_0:def 10; verum