let A1, A2 be set ; :: thesis: ( ( for x being set holds

( x in A1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) & ( for x being set holds

( x in A2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) implies A1 = A2 )

assume A22: for x being set holds

( x in A1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ; :: thesis: ( ex x being set st

( ( x in A2 implies ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) implies ( ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) & not x in A2 ) ) or A1 = A2 )

assume A23: for x being set holds

( x in A2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ; :: thesis: A1 = A2

A24: A2 c= A1

( x in A1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) & ( for x being set holds

( x in A2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ) implies A1 = A2 )

assume A22: for x being set holds

( x in A1 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ; :: thesis: ( ex x being set st

( ( x in A2 implies ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) implies ( ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) & not x in A2 ) ) or A1 = A2 )

assume A23: for x being set holds

( x in A2 iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) ; :: thesis: A1 = A2

A24: A2 c= A1

proof

A1 c= A2
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A2 or a in A1 )

assume a in A2 ; :: thesis: a in A1

then ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) by A23;

hence a in A1 by A22; :: thesis: verum

end;assume a in A2 ; :: thesis: a in A1

then ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) by A23;

hence a in A1 by A22; :: thesis: verum

proof

hence
A1 = A2
by A24, XBOOLE_0:def 10; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A1 or a in A2 )

assume a in A1 ; :: thesis: a in A2

then ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) by A22;

hence a in A2 by A23; :: thesis: verum

end;assume a in A1 ; :: thesis: a in A2

then ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st

( M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) by A22;

hence a in A2 by A23; :: thesis: verum