defpred S1[ object ] means ex msf being ManySortedFunction of U1,U1 st
( $1 = msf & msf is_homomorphism 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) & S1[x] ) )
from XBOOLE_0:sch 1();
( 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_homomorphism U1,U1 ) )
by AUTALG_1:20, MSUALG_3:9;
then reconsider X = X as non empty set by A1;
X c= MSFuncs ( the Sorts of U1, the Sorts of U1)
by A1;
then reconsider X = X as MSFunctionSet of U1,U1 ;
take
X
; ( ( 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
; for h being ManySortedFunction of U1,U1 holds
( h in X iff h is_homomorphism U1,U1 )
let h be ManySortedFunction of U1,U1; ( h in X iff h is_homomorphism U1,U1 )
h in MSFuncs ( the Sorts of U1, the Sorts of U1)
by AUTALG_1:20;
hence
( h is_homomorphism U1,U1 implies h in X )
by A1; verum