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 A7, PBOOLE:def 15;
A9: x1 in dom SA by A5, A7, PARTFUN1:def 2;
SA . x1 c= PFuncs (NAT,A)
proof
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
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 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;
hence a in PFuncs (NAT,A) by A11, PARTFUN1:def 3; :: thesis: verum
end;
then A17: dom Cm 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;
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 A1, A5, A6, FUNCT_2:def 2; :: thesis: verum