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

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)

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: verum

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

then reconsider SM9 = SM as Function of the carrier of S,(bool A) by FUNCT_2:6;
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;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

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

SM9 in Funcs ( the carrier of S,(bool A))
by FUNCT_2:8;
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 A7, PBOOLE:def 15;

A9: x1 in dom SA by A5, A7, PARTFUN1:def 2;

SA . x1 c= PFuncs (NAT,A)

x1 in dom SR by A5, A7, PARTFUN1:def 2;

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 A7, FUNCT_2:5;

then SR . x1 in rng the Sorts of M by A3, A18, FUNCT_1:def 3;

then rng Cm c= A by A4, XBOOLE_1:1;

hence x in PFuncs ((PFuncs (NAT,A)),A) by A8, A17, PARTFUN1:def 3; :: thesis: verum

end;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 A7, PBOOLE:def 15;

A9: x1 in dom SA by A5, A7, PARTFUN1:def 2;

SA . x1 c= PFuncs (NAT,A)

proof

then A17:
dom Cm c= PFuncs (NAT,A)
;
reconsider AX = the Arity of S . x1 as Element of the carrier of S * by A7, FUNCT_2:5;

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 A9, FUNCT_1:12;

( 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 A10, CARD_3:def 5;

then reconsider a9 = a as Function ;

rng AX c= dom the Sorts of M by A3;

then A12: dom a9 = dom AX by A11, RELAT_1:27;

rng a9 c= A

end;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 A9, FUNCT_1:12;

( 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 A10, CARD_3:def 5;

then reconsider a9 = a as Function ;

rng AX c= dom the Sorts of M by A3;

then A12: dom a9 = dom AX by A11, RELAT_1:27;

rng a9 c= A

proof

hence
a in PFuncs (NAT,A)
by A11, PARTFUN1:def 3; :: thesis: verum
rng the Sorts of M c= bool A

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 A12, A14, FUNCT_1:def 3;

then A16: the Sorts of M . (AX . r1) in rng the Sorts of M by A3, FUNCT_1:def 3;

r in ( the Sorts of M * AX) . r1 by A11, A14, A15;

then r in the Sorts of M . (AX . r1) by A12, A14, FUNCT_1:13;

then r in union (rng the Sorts of M) by A16, TARSKI:def 4;

then r in union (bool A) by A13;

hence r in A by ZFMISC_1:81; :: thesis: verum

end;proof

then A13:
union (rng the Sorts of M) c= union (bool A)
by ZFMISC_1:77;
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;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

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 A12, A14, FUNCT_1:def 3;

then A16: the Sorts of M . (AX . r1) in rng the Sorts of M by A3, FUNCT_1:def 3;

r in ( the Sorts of M * AX) . r1 by A11, A14, A15;

then r in the Sorts of M . (AX . r1) by A12, A14, FUNCT_1:13;

then r in union (rng the Sorts of M) by A16, TARSKI:def 4;

then r in union (bool A) by A13;

hence r in A by ZFMISC_1:81; :: thesis: verum

x1 in dom SR by A5, A7, PARTFUN1:def 2;

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 A7, FUNCT_2:5;

then SR . x1 in rng the Sorts of M by A3, A18, FUNCT_1:def 3;

then rng Cm c= A by A4, XBOOLE_1:1;

hence x in PFuncs ((PFuncs (NAT,A)),A) by A8, A17, PARTFUN1:def 3; :: thesis: verum

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: verum