defpred S_{1}[ 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 S_{1}[x,y] & S_{1}[x,z] holds

y = z

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)))):] & S_{1}[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

( M = $2 & $1 = [ the Sorts of M, the Charact of M] );

A1: for x, y, z being object st S

y = z

proof

consider X being set such that
let x, y, z be object ; :: thesis: ( S_{1}[x,y] & S_{1}[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 S_{1}[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;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 S

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

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)))):] & S

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 ) ) )

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

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)

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;( 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 )

given M being strict feasible MSAlgebra over S such that A13:
x = M
and ( 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: S_{1}[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

end;( 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: S

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;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

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

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 A14;

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 A14;

hence x in bool A ; :: thesis: verum

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

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;
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)

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;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

then A29:
dom Cm c= PFuncs (NAT,A)
;
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

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

hence
a in PFuncs (NAT,A)
by A23, 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

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;proof

then A25:
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 A14;

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 A14;

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

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

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

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