defpred S₁[ object ] means ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & $1 = f || X );
consider A being set such that
A1: for x being object holds
( x in A iff ( x in MSFuncs (X, the Sorts of C) & S₁[x] ) ) from XBOOLE_0:sch 1();
A c= MSFuncs (X, the Sorts of C) by A1;
then reconsider A = A as Subset of (MSFuncs (X, the Sorts of C)) ;
take A ; :: thesis: for s being ManySortedFunction of X, the Sorts of C holds
( s in A iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) )
let s be ManySortedFunction of X, the Sorts of C; :: thesis: ( s in A iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) )
X is_transformable_to the Sorts of C ;
hence ( s in A iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) by A1, AUTALG_1:20; :: thesis: verum