defpred S_{1}[ 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_{1}[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

( 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

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