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

A1: id the carrier of UA in { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism }

F is functional

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

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

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

assume h is_isomorphism ; :: 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_isomorphism }

proof

reconsider F = { x where x is Element of Funcs ( the carrier of UA, the carrier of UA) : x is_isomorphism } as set ;
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_isomorphism ) by Th1, 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_isomorphism } ; :: thesis: verum

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

F is functional

proof

then reconsider F = F as functional non empty set by A1;
let q be object ; :: according to FUNCT_1:def 13 :: thesis: ( not q in F or q is set )

assume q in F ; :: thesis: q is set

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

( q = x & x is_isomorphism ) ;

hence q is set ; :: thesis: verum

end;assume q in F ; :: thesis: q is set

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

( q = x & x is_isomorphism ) ;

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

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

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

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

thus ( h in F implies h is_isomorphism ) :: thesis: ( h is_isomorphism 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_isomorphism

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

( f = h & f is_isomorphism ) ;

hence h is_isomorphism ; :: thesis: verum

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

( f = h & f is_isomorphism ) ;

hence h is_isomorphism ; :: thesis: verum

assume h is_isomorphism ; :: thesis: h in F

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