defpred S₁[ set ] means ex msf being ManySortedFunction of U1,U1 st
( $1 = msf & msf is_homomorphism U1,U1 );
set T = the Sorts of U1;
consider X being set such that
A1: for x being set holds
( x in X iff ( x in product (MSFuncs the Sorts of U1,the Sorts of U1) & S₁[x] ) ) from XBOOLE_0:sch 1();
( id the Sorts of U1 in product (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_homomorphism U1,U1 ) ) by AUTALG_1:22, MSUALG_3:9;
then reconsider X = X as non empty set by A1;
X is MSFunctionSet of the Sorts of U1,the Sorts of U1

proof

thus the Sorts of U1 is_transformable_to the Sorts of U1 ; :: according to AUTALG_1:def 6 :: thesis: for b₁ being set holds
( not b₁ in X or b₁ is ManySortedFunction of the Sorts of U1,the Sorts of U1 )
let q be set ; :: thesis: ( not q in X or q is ManySortedFunction of the Sorts of U1,the Sorts of U1 )
assume q in X ; :: thesis: q is ManySortedFunction of the Sorts of U1,the Sorts of U1
then ex msf being ManySortedFunction of U1,U1 st
( q = msf & msf is_homomorphism U1,U1 ) by A1;
hence q is ManySortedFunction of the Sorts of U1,the Sorts of U1 ; :: thesis: verum

end;

then reconsider X = X as MSFunctionSet of the Sorts of U1,the Sorts of U1 ;
take X ; :: thesis: ( ( for f being Element of X holds f is ManySortedFunction of U1,U1 ) & ( for h being ManySortedFunction of U1,U1 holds
( h in X iff h is_homomorphism U1,U1 ) ) )
thus for f being Element of X holds f is ManySortedFunction of U1,U1 ; :: thesis: for h being ManySortedFunction of U1,U1 holds
( h in X iff h is_homomorphism U1,U1 )
let h be ManySortedFunction of U1,U1; :: thesis: ( h in X iff h is_homomorphism U1,U1 )

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

assume h in X ; :: thesis: h is_homomorphism U1,U1
then ex msf being ManySortedFunction of U1,U1 st
( h = msf & msf is_homomorphism U1,U1 ) by A1;
hence h is_homomorphism U1,U1 ; :: thesis: verum

end;

A2: h in product (MSFuncs the Sorts of U1,the Sorts of U1) by AUTALG_1:22;
assume h is_homomorphism U1,U1 ; :: thesis: h in X
hence h in X by A1, A2; :: thesis: verum