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

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

( 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 A2 or x in A1 )
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;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

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