set F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } ;
A1: id the carrier of UA in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA }

proof

set I = id the carrier of UA;
( id the carrier of UA in Funcs ( the carrier of UA, the carrier of UA) & id the carrier of UA is_homomorphism UA,UA ) by ALG_1:5, FUNCT_2:8;
hence id the carrier of UA in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } ; :: thesis: verum

end;

{ x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } is functional

proof

let q be set ; :: according to FUNCT_1:def 13 :: thesis: ( not q in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } or q is set )
assume q in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } ; :: thesis: q is set
then ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st
( q = x & x is_homomorphism UA,UA ) ;
hence q is set ; :: thesis: verum

end;

then reconsider F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism UA,UA } as functional non empty set by A1;
F is FUNCTION_DOMAIN of the carrier of UA, the carrier of UA

proof

let a be Element of F; :: according to FUNCT_2:def 12 :: thesis: a is Element of bool [: the carrier of UA, the carrier of UA:]
a in F ;
then ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st
( a = x & x is_homomorphism UA,UA ) ;
hence a is Element of bool [: the carrier of UA, the carrier of UA:] ; :: thesis: verum

end;

then reconsider F = F as FUNCTION_DOMAIN of the carrier of UA, the carrier of UA ;
take F ; :: thesis: for h being Function of UA,UA holds
( h in F iff h is_homomorphism UA,UA )
let h be Function of UA,UA; :: thesis: ( h in F iff h is_homomorphism UA,UA )
thus ( h in F implies h is_homomorphism UA,UA ) :: thesis: ( h is_homomorphism UA,UA implies h in F )

proof

assume h in F ; :: thesis: h is_homomorphism UA,UA
then ex f being Element of Funcs ( the carrier of UA, the carrier of UA) st
( f = h & f is_homomorphism UA,UA ) ;
hence h is_homomorphism UA,UA ; :: thesis: verum

end;

A2: h is Element of Funcs ( the carrier of UA, the carrier of UA) by FUNCT_2:8;
assume h is_homomorphism UA,UA ; :: thesis: h in F
hence h in F by A2; :: thesis: verum