defpred S1[ 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) & S1[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
; 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; ( 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; verum