defpred S_{1}[ object ] means ex msf being ManySortedFunction of U1,U1 st

( $1 = msf & msf is_isomorphism U1,U1 );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in MSFuncs ( the Sorts of U1, the Sorts of U1) & S_{1}[x] ) )
from XBOOLE_0:sch 1();

A2: X c= MSFuncs ( the Sorts of U1, the Sorts of U1) by A1;

( id the Sorts of U1 in MSFuncs ( the Sorts of U1, the Sorts of U1) & ex F being ManySortedFunction of U1,U1 st

( id the Sorts of U1 = F & F is_isomorphism U1,U1 ) ) by Th20, MSUALG_3:16;

then reconsider X = X as MSFunctionSet of U1,U1 by A1, A2;

take X ; :: thesis: for h being ManySortedFunction of U1,U1 holds

( h in X iff h is_isomorphism U1,U1 )

let h be ManySortedFunction of U1,U1; :: thesis: ( h in X iff h is_isomorphism U1,U1 )

hence ( h is_isomorphism U1,U1 implies h in X ) by A1; :: thesis: verum

( $1 = msf & msf is_isomorphism U1,U1 );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in MSFuncs ( the Sorts of U1, the Sorts of U1) & S

A2: X c= MSFuncs ( the Sorts of U1, the Sorts of U1) by A1;

( id the Sorts of U1 in MSFuncs ( the Sorts of U1, the Sorts of U1) & ex F being ManySortedFunction of U1,U1 st

( id the Sorts of U1 = F & F is_isomorphism U1,U1 ) ) by Th20, MSUALG_3:16;

then reconsider X = X as MSFunctionSet of U1,U1 by A1, A2;

take X ; :: thesis: for h being ManySortedFunction of U1,U1 holds

( h in X iff h is_isomorphism U1,U1 )

let h be ManySortedFunction of U1,U1; :: thesis: ( h in X iff h is_isomorphism U1,U1 )

hereby :: thesis: ( h is_isomorphism U1,U1 implies h in X )

h in MSFuncs ( the Sorts of U1, the Sorts of U1)
by Th20;assume
h in X
; :: thesis: h is_isomorphism U1,U1

then ex msf being ManySortedFunction of U1,U1 st

( h = msf & msf is_isomorphism U1,U1 ) by A1;

hence h is_isomorphism U1,U1 ; :: thesis: verum

end;then ex msf being ManySortedFunction of U1,U1 st

( h = msf & msf is_isomorphism U1,U1 ) by A1;

hence h is_isomorphism U1,U1 ; :: thesis: verum

hence ( h is_isomorphism U1,U1 implies h in X ) by A1; :: thesis: verum