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

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 }

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

let h be Function of UA,UA; :: thesis: ( h in F iff h is_homomorphism )

thus ( h in F implies h is_homomorphism ) :: thesis: ( h is_homomorphism implies h in F )

assume h is_homomorphism ; :: thesis: h in F

hence h in F by A2; :: thesis: verum

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 }

proof

{ x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism } is functional
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 ) 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 } ; :: thesis: verum

end;( id the carrier of UA in Funcs ( the carrier of UA, the carrier of UA) & id the carrier of UA is_homomorphism ) 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 } ; :: thesis: verum

proof

then reconsider F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism } as functional non empty set by A1;
let q be object ; :: 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 } 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 } ; :: 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 ) ;

hence q is set ; :: thesis: verum

end;assume q in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_homomorphism } ; :: 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 ) ;

hence q is set ; :: thesis: verum

F is FUNCTION_DOMAIN of the carrier of UA, the carrier of UA

proof

then reconsider F = F as FUNCTION_DOMAIN of the carrier of UA, the carrier of UA ;
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 ) ;

hence a is Element of bool [: the carrier of UA, the carrier of UA:] ; :: thesis: verum

end;a in F ;

then ex x being Element of Funcs ( the carrier of UA, the carrier of UA) st

( a = x & x is_homomorphism ) ;

hence a is Element of bool [: the carrier of UA, the carrier of UA:] ; :: thesis: verum

take F ; :: thesis: for h being Function of UA,UA holds

( h in F iff h is_homomorphism )

let h be Function of UA,UA; :: thesis: ( h in F iff h is_homomorphism )

thus ( h in F implies h is_homomorphism ) :: thesis: ( h is_homomorphism implies h in F )

proof

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

then ex f being Element of Funcs ( the carrier of UA, the carrier of UA) st

( f = h & f is_homomorphism ) ;

hence h is_homomorphism ; :: thesis: verum

end;then ex f being Element of Funcs ( the carrier of UA, the carrier of UA) st

( f = h & f is_homomorphism ) ;

hence h is_homomorphism ; :: thesis: verum

assume h is_homomorphism ; :: thesis: h in F

hence h in F by A2; :: thesis: verum