defpred S₁[ set , set ] means ex M, N being strict feasible MSAlgebra of S ex F being ManySortedFunction of M,N st
( $2 = F & i = M & j = N & $1 = [the Sorts of M,the Charact of M,the Sorts of N,the Charact of N,F] & the Sorts of M is_transformable_to the Sorts of N & F is_homomorphism M,N );
A2: for x, y, z being set st S₁[x,y] & S₁[x,z] holds
y = z by MCART_2:7;
consider X being set such that
A3: for x being set holds
( x in X iff ex y being set st
( y in [:(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)),(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)),(Funcs the carrier of S,(PFuncs (union (bool A)),(union (bool A)))):] & S₁[y,x] ) ) from TARSKI:sch 1(A2);
take X ; :: thesis:
thus for x being set holds
( x in X iff ex M, N being strict feasible MSAlgebra of 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:

let x be set ; :: thesis:

hereby :: thesis:

assume x in X ; :: thesis:
then consider y being set such that
A4: ( y in [:(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)),(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)),(Funcs the carrier of S,(PFuncs (union (bool A)),(union (bool A)))):] & S₁[y,x] ) by A3;
consider M, N being strict feasible MSAlgebra of S, F being ManySortedFunction of M,N such that
A5: ( x = F & i = M & j = N & y = [the Sorts of M,the Charact of M,the Sorts of N,the Charact of N,F] & the Sorts of M is_transformable_to the Sorts of N & F is_homomorphism M,N ) by A4;
thus ex M, N being strict feasible MSAlgebra of 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 ) by A5; :: thesis:

end;

given M, N being strict feasible MSAlgebra of S, F being ManySortedFunction of M,N such that A6: ( M = i & N = j & F = x & the Sorts of M is_transformable_to the Sorts of N & F is_homomorphism M,N ) ; :: thesis:
set y = [the Sorts of M,the Charact of M,the Sorts of N,the Charact of N,F];
[the Sorts of M,the Charact of M,the Sorts of N,the Charact of N,F] in [:(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)),(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)),(Funcs the carrier of S,(PFuncs (union (bool A)),(union (bool A)))):]

A7: the Sorts of M in Funcs the carrier of S,(bool A) by A1, A6, Th2;
A8: the Charact of M in Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A) by A1, A6, Th2;
A9: the Sorts of N in Funcs the carrier of S,(bool A) by A1, A6, Th2;
A10: the Charact of N in Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A) by A1, A6, Th2;
A11: dom F = the carrier of S by PARTFUN1:def 4;
rng F c= PFuncs (union (bool A)),(union (bool A))

let w be set ; :: according to TARSKI:def 3 :: thesis:
assume w in rng F ; :: thesis:
then consider w1 being set such that
A12: ( w1 in dom F & w = F . w1 ) by FUNCT_1:def 5;
A13: ( dom the Sorts of N = the carrier of S & dom the Sorts of M = the carrier of S ) by PARTFUN1:def 4;
reconsider w' = w as Function of (the Sorts of M . w1),(the Sorts of N . w1) by A11, A12, PBOOLE:def 18;
consider M' being strict feasible MSAlgebra of S such that
A14: ( M' = M & ( for C being Component of the Sorts of M' holds C c= A ) ) by A1, A6, Def2;
A15: rng the Sorts of M c= bool A

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng the Sorts of M ; :: thesis:
then reconsider x' = x as Component of the Sorts of M ;
x' c= A by A14;
hence x in bool A ; :: thesis:

end;

consider N' being strict feasible MSAlgebra of S such that
A16: ( N' = N & ( for C being Component of the Sorts of N' holds C c= A ) ) by A1, A6, Def2;
A17: rng the Sorts of N c= bool A

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng the Sorts of N ; :: thesis:
then reconsider x' = x as Component of the Sorts of N ;
x' c= A by A16;
hence x in bool A ; :: thesis:

end;

A18: dom w' c= union (bool A)

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume A19: s in dom w' ; :: thesis:
the Sorts of M . w1 in rng the Sorts of M by A11, A12, A13, FUNCT_1:def 5;
hence s in union (bool A) by A15, A19, TARSKI:def 4; :: thesis:

end;

rng w' c= union (bool A)

let r be set ; :: according to TARSKI:def 3 :: thesis:
assume r in rng w' ; :: thesis:
then consider r1 being set such that
A20: ( r1 in dom w' & r = w' . r1 ) by FUNCT_1:def 5;
A21: r in rng w' by A20, FUNCT_1:def 5;
the Sorts of N . w1 in rng the Sorts of N by A11, A12, A13, FUNCT_1:def 5;
hence r in union (bool A) by A17, A21, TARSKI:def 4; :: thesis:

end;

hence w in PFuncs (union (bool A)),(union (bool A)) by A18, PARTFUN1:def 5; :: thesis:

end;

then F in Funcs the carrier of S,(PFuncs (union (bool A)),(union (bool A))) by A11, FUNCT_2:def 2;
hence [the Sorts of M,the Charact of M,the Sorts of N,the Charact of N,F] in [:(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)),(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)),(Funcs the carrier of S,(PFuncs (union (bool A)),(union (bool A)))):] by A7, A8, A9, A10, MCART_2:31; :: thesis:

end;

hence x in X by A3, A6; :: thesis:

end;