defpred S1[ object , object ] means ex M being strict feasible MSAlgebra over S st
( M = $2 & $1 = [ the Sorts of M, the Charact of M] );
A1: for x, y, z being object st S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be object ; :: thesis: ( S1[x,y] & S1[x,z] implies y = z )
given M being strict feasible MSAlgebra over S such that A2: M = y and
A3: x = [ the Sorts of M, the Charact of M] ; :: thesis: ( not S1[x,z] or y = z )
given N being strict feasible MSAlgebra over S such that A4: N = z and
A5: x = [ the Sorts of N, the Charact of N] ; :: thesis: y = z
the Sorts of M = the Sorts of N by A3, A5, XTUPLE_0:1;
hence y = z by A2, A3, A4, A5, XTUPLE_0:1; :: thesis: verum
end;
consider X being set such that
A6: for x being object holds
( x in X iff ex y being object st
( y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] & S1[y,x] ) ) from TARSKI:sch 1(A1);
 take X ; :: thesis: for x being object holds
( x in X iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )
thus for x being object holds
( x in X iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) :: thesis: verum
proof
let x be object ; :: thesis: ( x in X iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) )
hereby :: thesis: ( ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) implies x in X )
assume x in X ; :: thesis: ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) )
then consider y being object such that
A7: y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] and
A8: S1[y,x] by A6;
consider M being strict feasible MSAlgebra over S such that
A9: M = x and
y = [ the Sorts of M, the Charact of M] by A8;
take M = M; :: thesis: ( x = M & ( for C being Component of the Sorts of M holds C c= A ) )
thus x = M by A9; :: thesis: for C being Component of the Sorts of M holds C c= A
thus for C being Component of the Sorts of M holds C c= A :: thesis: verum
proof
let C be Component of the Sorts of M; :: thesis: C c= A
consider y1 being object such that
y1 in dom the Sorts of M and
A10: C = the Sorts of M . y1 by FUNCT_1:def 3;
the Sorts of M in Funcs ( the carrier of S,(bool A)) by A7, A8, A9, ZFMISC_1:87;
then consider f being Function such that
A11: the Sorts of M = f and
dom f = the carrier of S and
A12: rng f c= bool A by FUNCT_2:def 2;
f . y1 in rng f by A10, A11;
hence C c= A by A10, A11, A12; :: thesis: verum
end;
end;
given M being strict feasible MSAlgebra over S such that A13: x = M and
A14: for C being Component of the Sorts of M holds C c= A ; :: thesis: x in X
A15: 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;
A16: 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 A14;
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;
consider y being set such that
A17: y = [ the Sorts of M, the Charact of M] ;
A18: dom the Charact of M = the carrier' of S by PARTFUN1:def 2;
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
A19: x1 in dom the Charact of M and
A20: x = the Charact of M . x1 by FUNCT_1:def 3;
reconsider Cm = CM . x1 as Function of (SA . x1),(SR . x1) by A19, PBOOLE:def 15;
A21: x1 in dom SA by A18, A19, 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 A19, 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 A22: a in ( the Sorts of M #) . ( the Arity of S . x1) by A21, FUNCT_1:12;
( the Sorts of M #) . AX = product ( the Sorts of M * AX) by FINSEQ_2:def 5;
then A23: 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 A22, CARD_3:def 5;
then reconsider a9 = a as Function ;
rng AX c= dom the Sorts of M by A15;
then A24: dom a9 = dom AX by A23, 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 A14;
hence w in bool A ; :: thesis: verum
end;
then A25: 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
A26: r1 in dom a9 and
A27: r = a9 . r1 by FUNCT_1:def 3;
AX . r1 in rng AX by A24, A26, FUNCT_1:def 3;
then A28: the Sorts of M . (AX . r1) in rng the Sorts of M by A15, FUNCT_1:def 3;
r in ( the Sorts of M * AX) . r1 by A23, A26, A27;
then r in the Sorts of M . (AX . r1) by A24, A26, FUNCT_1:13;
then r in union (rng the Sorts of M) by A28, TARSKI:def 4;
then r in union (bool A) by A25;
hence r in A by ZFMISC_1:81; :: thesis: verum
end;
hence a in PFuncs (NAT,A) by A23, PARTFUN1:def 3; :: thesis: verum
end;
then A29: dom Cm c= PFuncs (NAT,A) ;
x1 in dom SR by A18, A19, PARTFUN1:def 2;
then A30: 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 A19, FUNCT_2:5;
then SR . x1 in rng the Sorts of M by A15, A30, FUNCT_1:def 3;
then rng Cm c= A by A16, XBOOLE_1:1;
hence x in PFuncs ((PFuncs (NAT,A)),A) by A20, A29, PARTFUN1:def 3; :: thesis: verum
end;
then ( SM9 in Funcs ( the carrier of S,(bool A)) & the Charact of M in Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A))) ) by A18, FUNCT_2:8, FUNCT_2:def 2;
then y in [:(Funcs ( the carrier of S,(bool A))),(Funcs ( the carrier' of S,(PFuncs ((PFuncs (NAT,A)),A)))):] by A17, ZFMISC_1:87;
hence x in X by A6, A13, A17; :: thesis: verum
end;