let A be non empty set ; :: thesis:
let S be non empty non void ManySortedSign ; :: thesis:
let x be MSAlgebra of S; :: thesis:
assume x in MSAlg_set S,A ; :: thesis:
then consider M being strict feasible MSAlgebra of S such that
A1: ( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) by Def2;
A2: 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;
A4: 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 A1;
hence x in bool A ; :: thesis:

end;

then reconsider SM' = SM as Function of the carrier of S,(bool A) by FUNCT_2:8;
A5: SM' in Funcs the carrier of S,(bool A) by FUNCT_2:11;
A6: 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
A7: ( 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 ;
A8: x1 in the carrier' of S by A7, PARTFUN1:def 4;
A9: ( x1 in dom SR & x1 in dom SA ) by A6, A7, PARTFUN1:def 4;
reconsider Cm = CM . x1 as Function of (SA . x1),(SR . x1) by A6, A7, PBOOLE:def 18;
A10: the ResultSort of S . x1 in the carrier of S by A6, A7, FUNCT_2:7;
SR . x1 = the Sorts of M . (the ResultSort of S . x1) by A9, FUNCT_1:22;
then A11: SR . x1 in rng the Sorts of M by A2, A10, 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 A12: a in (the Sorts of M # ) . (the Arity of S . x1) by A9, FUNCT_1:22;
reconsider AX = the Arity of S . x1 as Element of the carrier of S * by A8, 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
A13: ( 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 A12, CARD_3:def 5;
reconsider a' = a as Function by A13;
rng AX c= dom the Sorts of M by A2;
then A14: dom a' = dom AX by A13, 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
A15: ( r1 in dom a' & r = a' . r1 ) by FUNCT_1:def 5;
r in (the Sorts of M * AX) . r1 by A13, A15;
then A16: r in the Sorts of M . (AX . r1) by A14, A15, 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 A1;
hence w in bool A ; :: thesis:

end;

then A17: union (rng the Sorts of M) c= union (bool A) by ZFMISC_1:95;
AX . r1 in rng AX by A14, A15, FUNCT_1:def 5;
then the Sorts of M . (AX . r1) in rng the Sorts of M by A2, FUNCT_1:def 5;
then r in union (rng the Sorts of M) by A16, TARSKI:def 4;
then r in union (bool A) by A17;
hence r in A by ZFMISC_1:99; :: thesis:

end;

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

end;

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

end;

hence ( the Sorts of x in Funcs the carrier of S,(bool A) & the Charact of x in Funcs the carrier' of S,(PFuncs (PFuncs NAT ,A),A) ) by A1, A5, A6, FUNCT_2:def 2; :: thesis: