let A1, A2 be Subset of (MSFuncs (X, the Sorts of C)); :: thesis: ( ( for s being ManySortedFunction of X, the Sorts of C holds
( s in A1 iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) ) & ( for s being ManySortedFunction of X, the Sorts of C holds
( s in A2 iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) ) implies A1 = A2 )
assume that
A2: for s being ManySortedFunction of X, the Sorts of C holds
( s in A1 iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) and
A3: for s being ManySortedFunction of X, the Sorts of C holds
( s in A2 iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) ; :: thesis: A1 = A2
A4: X is_transformable_to the Sorts of C ;
thus A1 c= A2 :: according to XBOOLE_0:def 10 :: thesis: A2 c= A1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A1 or x in A2 )
assume A5: x in A1 ; :: thesis: x in A2
then reconsider x = x as ManySortedFunction of X, the Sorts of C by A4, AUTALG_1:19;
ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & x = f || X ) by A2, A5;
hence x in A2 by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A2 or x in A1 )
assume A6: x in A2 ; :: thesis: x in A1
then reconsider x = x as ManySortedFunction of X, the Sorts of C by A4, AUTALG_1:19;
ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & x = f || X ) by A3, A6;
hence x in A1 by A2; :: thesis: verum