set X = { x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st
( x = h & h is one-to-one & h is onto ) } ;
A1: id the carrier of G in { x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st
( x = h & h is one-to-one & h is onto ) }

proof

set I = id the carrier of G;
A2: id the carrier of G in Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
reconsider I = id the carrier of G as Homomorphism of G,G by GROUP_6:38;
rng I = the carrier of G by RELAT_1:45;
then I is onto ;
hence id the carrier of G in { x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st
( x = h & h is one-to-one & h is onto ) } by A2; :: thesis: verum

end;

reconsider X = { x where x is Element of Funcs ( the carrier of G, the carrier of G) : ex h being Homomorphism of G,G st
( x = h & h is one-to-one & h is onto ) } as set ;
X is functional

proof

let q be object ; :: according to FUNCT_1:def 13 :: thesis: ( not q in X or q is set )
assume q in X ; :: thesis: q is set
then ex x being Element of Funcs ( the carrier of G, the carrier of G) st
( q = x & ex h being Homomorphism of G,G st
( h = x & h is one-to-one & h is onto ) ) ;
hence q is set ; :: thesis: verum

end;

then reconsider X = X as functional non empty set by A1;
X is FUNCTION_DOMAIN of the carrier of G, the carrier of G

proof

let a be Element of X; :: according to FUNCT_2:def 12 :: thesis: a is Element of bool [: the carrier of G, the carrier of G:]
a in X ;
then ex x being Element of Funcs ( the carrier of G, the carrier of G) st
( a = x & ex h being Homomorphism of G,G st
( h = x & h is one-to-one & h is onto ) ) ;
hence a is Element of bool [: the carrier of G, the carrier of G:] ; :: thesis: verum

end;

then reconsider X = X as FUNCTION_DOMAIN of the carrier of G, the carrier of G ;
take X ; :: thesis: ( ( for f being Element of X holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in X iff ( h is one-to-one & h is onto ) ) ) )

hereby :: thesis: for h being Homomorphism of G,G holds
( h in X iff ( h is one-to-one & h is onto ) )

let f be Element of X; :: thesis: f is Homomorphism of G,G
f in X ;
then ex x being Element of Funcs ( the carrier of G, the carrier of G) st
( f = x & ex h being Homomorphism of G,G st
( h = x & h is one-to-one & h is onto ) ) ;
hence f is Homomorphism of G,G ; :: thesis: verum

end;

let x be Homomorphism of G,G; :: thesis: ( x in X iff ( x is one-to-one & x is onto ) )

hereby :: thesis: ( x is one-to-one & x is onto implies x in X )

assume x in X ; :: thesis: ( x is one-to-one & x is onto )
then ex f being Element of Funcs ( the carrier of G, the carrier of G) st
( f = x & ex h being Homomorphism of G,G st
( h = f & h is one-to-one & h is onto ) ) ;
hence ( x is one-to-one & x is onto ) ; :: thesis: verum

end;

A3: x is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
assume ( x is one-to-one & x is onto ) ; :: thesis: x in X
hence x in X by A3; :: thesis: verum