defpred S₁[ set , set ] means ex M being strict feasible MSAlgebra of S st
( M = $2 & $1 = [the Sorts of M,the Charact of M] );
A1: for x, y, z being set st S₁[x,y] & S₁[x,z] holds
y = z

let x, y, z be set ; :: thesis:
given M being strict feasible MSAlgebra of S such that A2: ( M = y & x = [the Sorts of M,the Charact of M] ) ; :: thesis:
given N being strict feasible MSAlgebra of S such that A3: ( N = z & x = [the Sorts of N,the Charact of N] ) ; :: thesis:
( the Sorts of M = the Sorts of N & the Charact of M = the Charact of N ) by A2, A3, ZFMISC_1:33;
hence y = z by A2, A3; :: thesis:

end;

consider X being set such that
A4: 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)):] & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take X ; :: thesis:
thus for x being set holds
( x in X iff ex M being strict feasible MSAlgebra of S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) :: thesis:

let x be set ; :: thesis:

hereby :: thesis:

assume x in X ; :: thesis:
then consider y being set such that
A5: ( y in [:(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)):] & S₁[y,x] ) by A4;
consider M being strict feasible MSAlgebra of S such that
A6: ( M = x & y = [the Sorts of M,the Charact of M] ) by A5;
take M = M; :: thesis:
thus x = M by A6; :: thesis:
thus for C being Component of the Sorts of M holds C c= A :: thesis:

let C be Component of the Sorts of M; :: thesis:

per cases ;

suppose not rng the Sorts of M is empty ; :: thesis:

reconsider RS = rng the Sorts of M as non empty set ;
consider y1 being set such that
A7: ( y1 in dom the Sorts of M & C = the Sorts of M . y1 ) by FUNCT_1:def 5;
the Sorts of M in Funcs the carrier of S,(bool A) by A5, A6, ZFMISC_1:106;
then consider f being Function such that
A8: ( the Sorts of M = f & dom f = the carrier of S & rng f c= bool A ) by FUNCT_2:def 2;
f . y1 in rng f by A7, A8;
hence C c= A by A7, A8; :: thesis:

end;

suppose rng the Sorts of M is empty ; :: thesis:

then dom the Sorts of M = {} ;
hence C c= A ; :: thesis:

end;

given M being strict feasible MSAlgebra of S such that A9: ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ; :: thesis:
consider y being set such that
A10: y = [the Sorts of M,the Charact of M] ;
A11: dom the Sorts of M = the carrier of S by PARTFUN1:def 4;
then reconsider SM = the Sorts of M as Function of the carrier of S,(rng the Sorts of M) by FUNCT_2:3;
A13: 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 A9;
hence x in bool A ; :: thesis:

end;

then reconsider SM' = SM as Function of the carrier of S,(bool A) by FUNCT_2:8;
A14: SM' in Funcs the carrier of S,(bool A) by FUNCT_2:11;
A15: dom the Charact of M = the carrier' of S by PARTFUN1:def 4;
rng the Charact of M c= PFuncs (PFuncs NAT ,A),A

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng the Charact of M ; :: thesis:
then consider x1 being set such that
A16: ( x1 in dom the Charact of M & x = the Charact of M . x1 ) by FUNCT_1:def 5;
reconsider SA = (the Sorts of M # ) * the Arity of S, SR = the Sorts of M * the ResultSort of S as ManySortedSet of ;
reconsider CM = the Charact of M as ManySortedFunction of SA,SR ;
A17: x1 in the carrier' of S by A16, PARTFUN1:def 4;
A18: ( x1 in dom SR & x1 in dom SA ) by A15, A16, PARTFUN1:def 4;
reconsider Cm = CM . x1 as Function of (SA . x1),(SR . x1) by A15, A16, PBOOLE:def 18;
A19: the ResultSort of S . x1 in the carrier of S by A15, A16, FUNCT_2:7;
SR . x1 = the Sorts of M . (the ResultSort of S . x1) by A18, FUNCT_1:22;
then A20: SR . x1 in rng the Sorts of M by A11, A19, FUNCT_1:def 5;
SA . x1 c= PFuncs NAT ,A

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in SA . x1 ; :: thesis:
then A21: a in (the Sorts of M # ) . (the Arity of S . x1) by A18, FUNCT_1:22;
reconsider AX = the Arity of S . x1 as Element of the carrier of S * by A17, FUNCT_2:7;
(the Sorts of M # ) . AX = product (the Sorts of M * AX) by PBOOLE:def 19;
then consider g being Function such that
A22: ( a = g & dom g = dom (the Sorts of M * AX) & ( for x2 being set st x2 in dom (the Sorts of M * AX) holds
g . x2 in (the Sorts of M * AX) . x2 ) ) by A21, CARD_3:def 5;
reconsider a' = a as Function by A22;
rng AX c= dom the Sorts of M by A11;
then A23: dom a' = dom AX by A22, RELAT_1:46;
rng a' c= A

let r be set ; :: according to TARSKI:def 3 :: thesis:
assume r in rng a' ; :: thesis:
then consider r1 being set such that
A24: ( r1 in dom a' & r = a' . r1 ) by FUNCT_1:def 5;
r in (the Sorts of M * AX) . r1 by A22, A24;
then A25: r in the Sorts of M . (AX . r1) by A23, A24, FUNCT_1:23;
rng the Sorts of M c= bool A

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

end;

then A26: union (rng the Sorts of M) c= union (bool A) by ZFMISC_1:95;
AX . r1 in rng AX by A23, A24, FUNCT_1:def 5;
then the Sorts of M . (AX . r1) in rng the Sorts of M by A11, FUNCT_1:def 5;
then r in union (rng the Sorts of M) by A25, TARSKI:def 4;
then r in union (bool A) by A26;
hence r in A by ZFMISC_1:99; :: thesis:

end;

hence a in PFuncs NAT ,A by A23, PARTFUN1:def 5; :: thesis:

end;

then ( dom Cm c= PFuncs NAT ,A & rng Cm c= A ) by A13, A20, XBOOLE_1:1;
hence x in PFuncs (PFuncs NAT ,A),A by A16, PARTFUN1:def 5; :: thesis:

end;

then the Charact of M in Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A) by A15, FUNCT_2:def 2;
then ( y in [:(Funcs the carrier of S,(bool A)),(Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A)):] & ex M being strict feasible MSAlgebra of S st
( M = x & y = [the Sorts of M,the Charact of M] ) ) by A9, A10, A14, ZFMISC_1:106;
hence x in X by A4; :: thesis:

end;