let A be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for x being MSAlgebra over S st x in MSAlg_set (S,A) holds
( 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))) )

let S be non empty non void ManySortedSign ; :: thesis: for x being MSAlgebra over S st x in MSAlg_set (S,A) holds
( 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))) )

let x be MSAlgebra over S; :: thesis: ( x in MSAlg_set (S,A) implies ( 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))) ) )
assume x in MSAlg_set (S,A) ; :: thesis: ( 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))) )
then consider M being strict feasible MSAlgebra over S such that
A1: x = M and
A2: for C being Component of the Sorts of M holds C c= A by Def2;
A3: dom the Sorts of M = the carrier of S by PARTFUN1:def 2;
then reconsider SM = the Sorts of M as Function of the carrier of S,(rng the Sorts of M) by FUNCT_2:1;
A4: rng the Sorts of M c= bool A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng the Sorts of M or x in bool A )
assume x in rng the Sorts of M ; :: thesis: x in bool A
then reconsider x9 = x as Component of the Sorts of M ;
x9 c= A by A2;
hence x in bool A ; :: thesis: verum
end;
then reconsider SM9 = SM as Function of the carrier of S,(bool A) by FUNCT_2:6;
A5: dom the Charact of M = the carrier' of S by PARTFUN1:def 2;
A6: rng the Charact of M c= PFuncs ((PFuncs (NAT,A)),A)
proof
reconsider SA = ( the Sorts of M #) * the Arity of S, SR = the Sorts of M * the ResultSort of S as ManySortedSet of the carrier' of S ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng the Charact of M or x in PFuncs ((PFuncs (NAT,A)),A) )
reconsider CM = the Charact of M as ManySortedFunction of SA,SR ;
assume x in rng the Charact of M ; :: thesis: x in PFuncs ((PFuncs (NAT,A)),A)
then consider x1 being object such that
A7: x1 in dom the Charact of M and
A8: x = the Charact of M . x1 by FUNCT_1:def 3;
reconsider Cm = CM . x1 as Function of (SA . x1),(SR . x1) by ;
A9: x1 in dom SA by ;
SA . x1 c= PFuncs (NAT,A)
proof
reconsider AX = the Arity of S . x1 as Element of the carrier of S * by ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in SA . x1 or a in PFuncs (NAT,A) )
assume a in SA . x1 ; :: thesis: a in PFuncs (NAT,A)
then A10: a in ( the Sorts of M #) . ( the Arity of S . x1) by ;
( the Sorts of M #) . AX = product ( the Sorts of M * AX) by FINSEQ_2:def 5;
then A11: ex g being Function st
( a = g & dom g = dom ( the Sorts of M * AX) & ( for x2 being object st x2 in dom ( the Sorts of M * AX) holds
g . x2 in ( the Sorts of M * AX) . x2 ) ) by ;
then reconsider a9 = a as Function ;
rng AX c= dom the Sorts of M by A3;
then A12: dom a9 = dom AX by ;
rng a9 c= A
proof
rng the Sorts of M c= bool A
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in rng the Sorts of M or w in bool A )
assume w in rng the Sorts of M ; :: thesis: w in bool A
then reconsider w9 = w as Component of the Sorts of M ;
w9 c= A by A2;
hence w in bool A ; :: thesis: verum
end;
then A13: union (rng the Sorts of M) c= union (bool A) by ZFMISC_1:77;
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in rng a9 or r in A )
assume r in rng a9 ; :: thesis: r in A
then consider r1 being object such that
A14: r1 in dom a9 and
A15: r = a9 . r1 by FUNCT_1:def 3;
AX . r1 in rng AX by ;
then A16: the Sorts of M . (AX . r1) in rng the Sorts of M by ;
r in ( the Sorts of M * AX) . r1 by ;
then r in the Sorts of M . (AX . r1) by ;
then r in union (rng the Sorts of M) by ;
then r in union (bool A) by A13;
hence r in A by ZFMISC_1:81; :: thesis: verum
end;
hence a in PFuncs (NAT,A) by ; :: thesis: verum
end;
then A17: dom Cm c= PFuncs (NAT,A) ;
x1 in dom SR by ;
then A18: SR . x1 = the Sorts of M . ( the ResultSort of S . x1) by FUNCT_1:12;
the ResultSort of S . x1 in the carrier of S by ;
then SR . x1 in rng the Sorts of M by ;
then rng Cm c= A by ;
hence x in PFuncs ((PFuncs (NAT,A)),A) by ; :: thesis: verum
end;
SM9 in Funcs ( the carrier of S,(bool A)) by FUNCT_2:8;
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 ; :: thesis: verum