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 ) }

( x = h & h is one-to-one & h is onto ) } as set ;

X is functional

X is 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 ) ) ) )

assume ( x is one-to-one & x is onto ) ; :: thesis: x in X

hence x in X by A3; :: thesis: verum

( 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

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
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;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

( x = h & h is one-to-one & h is onto ) } as set ;

X is functional

proof

then reconsider X = X as functional non empty set by A1;
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;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

X is FUNCTION_DOMAIN of the carrier of G, the carrier of G

proof

then reconsider X = X as FUNCTION_DOMAIN of the carrier of G, the carrier of G ;
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;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

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 x be Homomorphism of G,G; :: thesis: ( x in X iff ( x is one-to-one & x is onto ) )( 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;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

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

A3:
x is Element of Funcs ( the carrier of G, the carrier of G)
by FUNCT_2:8;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;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

assume ( x is one-to-one & x is onto ) ; :: thesis: x in X

hence x in X by A3; :: thesis: verum