:: REWRITE3 semantic presentation

REAL is V77() V78() V79() V83() set
NAT is V6() non finite V37() V38() V77() V78() V79() V80() V81() V82() V83() Element of bool REAL
bool REAL is non empty set
NAT is V6() non finite V37() V38() V77() V78() V79() V80() V81() V82() V83() set
bool NAT is non empty non finite set
bool NAT is non empty non finite set

1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
K201(NAT,0,1) is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
K201(NAT,0,1) ^omega is non empty functional set
bool (K201(NAT,0,1) ^omega) is non empty set

bool is non empty set
2 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
3 is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT

x is set

X is V6() V10() V11() ext-real non negative finite V37() V100() set
X + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set

dom E is V77() V78() V79() V80() V81() V82() Element of bool NAT

(<*x*> ^ E) . (X + 1) is set
E . X is set
len <*x*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
() + 0 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
() + X is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom (<*x*> ^ E) is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
len (<*x*> ^ E) is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(X + 1) - () is V11() ext-real V100() set
E . ((X + 1) - ()) is set
(X + 1) - 1 is V11() ext-real V100() set
E . ((X + 1) - 1) is set
1 - 1 is V11() ext-real V100() set
X + (1 - 1) is V11() ext-real V100() set
E . (X + (1 - 1)) is set

len x is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT

E is set

len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len X) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
len <*E*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len X) + () is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
x is V6() V10() V11() ext-real non negative finite V37() V100() set
x + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set

dom X is V77() V78() V79() V80() V81() V82() Element of bool NAT
len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
1 + 0 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set

len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom E is V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
E . (F2 + 1) is set
(E ^ F1) . (F2 + 1) is set
len X is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom X is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
E . F2 is set
(E ^ F1) . F2 is set
[(E . F2),(E . (F2 + 1))] is V26() set
{(E . F2),(E . (F2 + 1))} is non empty set
{(E . F2)} is non empty trivial V39(1) set
{{(E . F2),(E . (F2 + 1))},{(E . F2)}} is non empty set
F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom F1 is V77() V78() V79() V80() V81() V82() Element of bool NAT
F2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
(F2 + 1) + (len E) is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F2 + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
F1 . (F2 + 1) is set
(len E) + (F2 + 1) is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
(E ^ F1) . ((len E) + (F2 + 1)) is set
(len E) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) - (len F1) is V11() ext-real V100() set
((len X) - (len F1)) + (len F1) is V11() ext-real V100() set
(len E) + F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
((len E) + F2) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
F1 . F2 is set
(E ^ F1) . ((len E) + F2) is set
[(F1 . F2),(F1 . (F2 + 1))] is V26() set
{(F1 . F2),(F1 . (F2 + 1))} is non empty set
{(F1 . F2)} is non empty trivial V39(1) set
{{(F1 . F2),(F1 . (F2 + 1))},{(F1 . F2)}} is non empty set

len X is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
X . 1 is set

E is set

len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len F1) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + (len F1) is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + 0 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
len <*E*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT

len X is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
X . (len X) is set

F1 is set

len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len E) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + (len E) is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
1 + 0 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
len <*F1*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT

len X is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
X . 1 is set

len E is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
(len E) + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
dom E is non empty V77() V78() V79() V80() V81() V82() Element of bool NAT
F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
E . F1 is set
F1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
X . (F1 + 1) is set
x is set
X is set

[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set

<*x,X*> . 1 is set
<*x,X*> . 2 is set
len <*x,X*> is non empty V6() V10() V11() ext-real positive non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
dom <*x,X*> is non empty V39(2) V77() V78() V79() V80() V81() V82() Element of bool NAT
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite V37() V100() set
x is non empty set
x ^omega is non empty functional set

len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set

len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 E is V6() V10() V11() ext-real non negative finite V37() V100() set

K266(x) is non empty functional M12(x)
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len E) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
((len E) + (len F1)) + 0 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
x is non empty set
x ^omega is non empty functional set

K266(x) is non empty functional M12(x)

len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set

len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 E is V6() V10() V11() ext-real non negative finite V37() V100() set

len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len E) + (len F1) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
((len E) + (len F1)) + 0 is V6() V10() V11() ext-real non negative finite V37() V100() set
x is non empty set
x ^omega is non empty functional set

len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set

K266(x) is non empty functional M12(x)
len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 E is V6() V10() V11() ext-real non negative finite V37() V100() set

len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set

F1 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
len F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
len (F1 ^ F2) is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 (F1 ^ F2) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len F1) + (len F2) is V6() V10() V11() ext-real non negative finite V37() V100() set
TS1 is V6() V10() V11() ext-real non negative finite V37() V100() set
dom X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of bool NAT
X . TS1 is set
(F1 ^ F2) . TS1 is set
F1 . TS1 is set
x is non empty set
x ^omega is non empty functional set

len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set

K266(x) is non empty functional M12(x)
len E is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 E is V6() V10() V11() ext-real non negative finite V37() V100() set

len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set

F1 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
len F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
(len X) + (len E) is V6() V10() V11() ext-real non negative finite V37() V100() set
len (F1 ^ F2) is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 (F1 ^ F2) is V6() V10() V11() ext-real non negative finite V37() V100() set
(len F1) + (len F2) is V6() V10() V11() ext-real non negative finite V37() V100() set
((len X) + (len E)) - (len E) is V11() ext-real V100() set
((len F1) + (len F2)) - (len F2) is V11() ext-real V100() set

X ^ TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
TS2 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
X ^ (TS2 ^ F2) is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
x is non empty set
x ^omega is non empty functional set

K266(x) is non empty functional M12(x)

F1 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set
len X is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 X is V6() V10() V11() ext-real non negative finite V37() V100() set
x is non empty set
x ^omega is non empty functional set
bool () is non empty set
X is functional Element of bool ()
x is non empty set
x ^omega is non empty functional set
bool () is non empty set
X is functional Element of bool ()
E is (X)
the of E is Relation-like [: the carrier of E,X:] -defined the carrier of E -valued Element of bool [:[: the carrier of E,X:], the carrier of E:]
the carrier of E is set
[: the carrier of E,X:] is Relation-like set
[:[: the carrier of E,X:], the carrier of E:] is Relation-like set
bool [:[: the carrier of E,X:], the carrier of E:] is non empty set
proj1 the of E is Relation-like set

F1 is Element of the carrier of E
[F1,F2] is V26() set
{F1,F2} is non empty set
{F1} is non empty trivial V39(1) set
{{F1,F2},{F1}} is non empty set
[F1,TS1] is V26() set
{F1,TS1} is non empty set
{{F1,TS1},{F1}} is non empty set

F2 ^ TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
K266(x) is non empty functional M12(x)

TS1 ^ y is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(x)
x is non empty set
x ^omega is non empty functional set
bool () is non empty set
X is functional Element of bool ()
the non empty finite set is non empty finite set
[: the non empty finite set ,X:] is Relation-like set
[:[: the non empty finite set ,X:], the non empty finite set :] is Relation-like set
bool [:[: the non empty finite set ,X:], the non empty finite set :] is non empty set
F1 is Relation-like [: the non empty finite set ,X:] -defined the non empty finite set -valued Element of bool [:[: the non empty finite set ,X:], the non empty finite set :]
(X, the non empty finite set ,F1) is (X) (X)
F2 is (X) (X)
the carrier of F2 is set
x is set
x is set
X is set
E is set
F1 is set
F2 is (x)
the of F2 is Relation-like [: the carrier of F2,x:] -defined the carrier of F2 -valued Element of bool [:[: the carrier of F2,x:], the carrier of F2:]
the carrier of F2 is set
[: the carrier of F2,x:] is Relation-like set
[:[: the carrier of F2,x:], the carrier of F2:] is Relation-like set
bool [:[: the carrier of F2,x:], the carrier of F2:] is non empty set
proj1 the of F2 is Relation-like set
proj1 (proj1 the of F2) is set
proj2 (proj1 the of F2) is set
proj2 the of F2 is set
[X,E] is V26() set
{X,E} is non empty set
{X} is non empty trivial V39(1) set
{{X,E},{X}} is non empty set
[[X,E],F1] is V26() set
{[X,E],F1} is non empty set
{[X,E]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[X,E],F1},{[X,E]}} is non empty set
x is set
X is set
E is set
F1 is set
F2 is set
TS1 is (x)
the of TS1 is Relation-like [: the carrier of TS1,x:] -defined the carrier of TS1 -valued Element of bool [:[: the carrier of TS1,x:], the carrier of TS1:]
the carrier of TS1 is set
[: the carrier of TS1,x:] is Relation-like set
[:[: the carrier of TS1,x:], the carrier of TS1:] is Relation-like set
bool [:[: the carrier of TS1,x:], the carrier of TS1:] is non empty set
TS2 is (X)
the of TS2 is Relation-like [: the carrier of TS2,X:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,X:], the carrier of TS2:]
the carrier of TS2 is set
[: the carrier of TS2,X:] is Relation-like set
[:[: the carrier of TS2,X:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,X:], the carrier of TS2:] is non empty set
[E,F1] is V26() set
{E,F1} is non empty set
{E} is non empty trivial V39(1) set
{{E,F1},{E}} is non empty set
[[E,F1],F2] is V26() set
{[E,F1],F2} is non empty set
{[E,F1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[E,F1],F2},{[E,F1]}} is non empty set
x is set
X is set
E is set
F1 is set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is (TS1)
the of TS2 is Relation-like [: the carrier of TS2,TS1:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,TS1:], the carrier of TS2:]
the carrier of TS2 is set
[: the carrier of TS2,TS1:] is Relation-like set
[:[: the carrier of TS2,TS1:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,TS1:], the carrier of TS2:] is non empty set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
[[x,X],E] is V26() set
{[x,X],E} is non empty set
{[x,X]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,X],E},{[x,X]}} is non empty set
[[x,X],F1] is V26() set
{[x,X],F1} is non empty set
{{[x,X],F1},{[x,X]}} is non empty set
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set

K266(E) is non empty functional M12(E)
F1 is functional Element of bool ()
F2 is (F1)
the of F2 is Relation-like [: the carrier of F2,F1:] -defined the carrier of F2 -valued Element of bool [:[: the carrier of F2,F1:], the carrier of F2:]
the carrier of F2 is set
[: the carrier of F2,F1:] is Relation-like set
[:[: the carrier of F2,F1:], the carrier of F2:] is Relation-like set
bool [:[: the carrier of F2,F1:], the carrier of F2:] is non empty set
proj1 the of F2 is Relation-like set
proj2 (proj1 the of F2) is set
[x,(<%> E)] is V26() set
{x,(<%> E)} is non empty set
{x} is non empty trivial V39(1) set
{{x,(<%> E)},{x}} is non empty set
[[x,(<%> E)],X] is V26() set
{[x,(<%> E)],X} is non empty set
{[x,(<%> E)]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,(<%> E)],X},{[x,(<%> E)]}} is non empty set
x is set
X is set
E is set
F1 is non empty set
F1 ^omega is non empty functional set
bool (F1 ^omega) is non empty set

TS2 is functional Element of bool (F1 ^omega)
y is (F1,TS2) (TS2)
the carrier of y is set
q is Element of the carrier of y
[q,TS1] is V26() set
{q,TS1} is non empty set
{q} is non empty trivial V39(1) set
{{q,TS1},{q}} is non empty set
[[q,TS1],E] is V26() set
{[q,TS1],E} is non empty set
{[q,TS1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[q,TS1],E},{[q,TS1]}} is non empty set
the of y is Relation-like [: the carrier of y,TS2:] -defined the carrier of y -valued Element of bool [:[: the carrier of y,TS2:], the carrier of y:]
[: the carrier of y,TS2:] is Relation-like set
[:[: the carrier of y,TS2:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y,TS2:], the carrier of y:] is non empty set
proj1 the of y is Relation-like set
[q,F2] is V26() set
{q,F2} is non empty set
{{q,F2},{q}} is non empty set
[[q,F2],X] is V26() set
{[q,F2],X} is non empty set
{[q,F2]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[q,F2],X},{[q,F2]}} is non empty set

F2 ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
K266(F1) is non empty functional M12(F1)

TS1 ^ q is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
x is non empty set
x ^omega is non empty functional set
bool () is non empty set
X is functional Element of bool ()
x is set
X is set
E is set
F1 is set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is (TS1)
the of TS2 is Relation-like [: the carrier of TS2,TS1:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,TS1:], the carrier of TS2:]
the carrier of TS2 is set
[: the carrier of TS2,TS1:] is Relation-like set
[:[: the carrier of TS2,TS1:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,TS1:], the carrier of TS2:] is non empty set
proj1 the of TS2 is Relation-like set
proj1 (proj1 the of TS2) is set
proj2 the of TS2 is set

K266(F2) is non empty functional M12(F2)
x is set
X is set
E is set
F1 is set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is functional Element of bool (F2 ^omega)
y is (TS1)
the of y is Relation-like [: the carrier of y,TS1:] -defined the carrier of y -valued Element of bool [:[: the carrier of y,TS1:], the carrier of y:]
the carrier of y is set
[: the carrier of y,TS1:] is Relation-like set
[:[: the carrier of y,TS1:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y,TS1:], the carrier of y:] is non empty set
q is (TS2)
the of q is Relation-like [: the carrier of q,TS2:] -defined the carrier of q -valued Element of bool [:[: the carrier of q,TS2:], the carrier of q:]
the carrier of q is set
[: the carrier of q,TS2:] is Relation-like set
[:[: the carrier of q,TS2:], the carrier of q:] is Relation-like set
bool [:[: the carrier of q,TS2:], the carrier of q:] is non empty set

K266(F2) is non empty functional M12(F2)
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set

TS1 is functional Element of bool ()
TS2 is (TS1)

K266(E) is non empty functional M12(E)

x is set
X is set
E is set
F1 is non empty set
F1 ^omega is non empty functional set
bool (F1 ^omega) is non empty set

K266(F1) is non empty functional M12(F1)
F2 is functional Element of bool (F1 ^omega)
TS1 is (F2)

y ^ TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set

F1 ^ F2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
K266(E) is non empty functional M12(E)
TS1 is functional Element of bool ()
TS2 is (TS1)

x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set

F1 ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
K266(E) is non empty functional M12(E)
F2 ^ TS1 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
TS2 is functional Element of bool ()
y is (TS2)

q ^ (F2 ^ TS1) is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(E)
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set

len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set

len F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
TS1 is functional Element of bool ()
TS2 is (TS1)

K266(E) is non empty functional M12(E)
x is set
X is set
E is set
F1 is set
F2 is set
TS1 is non empty set
TS1 ^omega is non empty functional set
bool (TS1 ^omega) is non empty set
TS2 is functional Element of bool (TS1 ^omega)
y is (TS2)
the of y is Relation-like [: the carrier of y,TS2:] -defined the carrier of y -valued Element of bool [:[: the carrier of y,TS2:], the carrier of y:]
the carrier of y is set
[: the carrier of y,TS2:] is Relation-like set
[:[: the carrier of y,TS2:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y,TS2:], the carrier of y:] is non empty set

p ^ q is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS1)
K266(TS1) is non empty functional M12(TS1)

p ^ q is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS1)
x is set
X is set
E is set
F1 is non empty set
F1 ^omega is non empty functional set
bool (F1 ^omega) is non empty set

K266(F1) is non empty functional M12(F1)
F2 is functional Element of bool (F1 ^omega)
TS1 is (F2)
the of TS1 is Relation-like [: the carrier of TS1,F2:] -defined the carrier of TS1 -valued Element of bool [:[: the carrier of TS1,F2:], the carrier of TS1:]
the carrier of TS1 is set
[: the carrier of TS1,F2:] is Relation-like set
[:[: the carrier of TS1,F2:], the carrier of TS1:] is Relation-like set
bool [:[: the carrier of TS1,F2:], the carrier of TS1:] is non empty set
proj1 the of TS1 is Relation-like set
proj2 (proj1 the of TS1) is set

y ^ TS2 is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(F1)
[x,y] is V26() set
{x,y} is non empty set
{x} is non empty trivial V39(1) set
{{x,y},{x}} is non empty set
[[x,y],E] is V26() set
{[x,y],E} is non empty set
{[x,y]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,y],E},{[x,y]}} is non empty set
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set

K266(E) is non empty functional M12(E)

len F1 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F1 is V6() V10() V11() ext-real non negative finite V37() V100() set

len F2 is V6() V10() V11() ext-real non negative finite V37() V77() V78() V79() V80() V81() V82() V100() Element of NAT
proj1 F2 is V6() V10() V11() ext-real non negative finite V37() V100() set
TS1 is functional Element of bool ()
TS2 is (TS1)
the of TS2 is Relation-like [: the carrier of TS2,TS1:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,TS1:], the carrier of TS2:]
the carrier of TS2 is set
[: the carrier of TS2,TS1:] is Relation-like set
[:[: the carrier of TS2,TS1:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,TS1:], the carrier of TS2:] is non empty set
proj1 the of TS2 is Relation-like set
proj2 (proj1 the of TS2) is set

x is set
X is set
E is set
F1 is set
F2 is set
TS1 is set
TS2 is non empty set
TS2 ^omega is non empty functional set
bool (TS2 ^omega) is non empty set
y is functional Element of bool (TS2 ^omega)
q is (TS2,y) (y)

q ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
K266(TS2) is non empty functional M12(TS2)

v ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
the of q is Relation-like [: the carrier of q,y:] -defined the carrier of q -valued Element of bool [:[: the carrier of q,y:], the carrier of q:]
the carrier of q is set
[: the carrier of q,y:] is Relation-like set
[:[: the carrier of q,y:], the carrier of q:] is Relation-like set
bool [:[: the carrier of q,y:], the carrier of q:] is non empty set

v ^ v is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
v ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)

q ^ l is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
l ^ p is V8() Relation-like NAT -defined Function-like finite V98() Element of K266(TS2)
x is non empty set
x ^omega is non empty functional set
bool () is non empty set
X is functional Element of bool ()
E is non empty (X)
the carrier of E is non empty set
[: the carrier of E,():] is non empty Relation-like set
[:[: the carrier of E,():],[: the carrier of E,():]:] is non empty Relation-like set
bool [:[: the carrier of E,():],[: the carrier of E,():]:] is non empty set
F1 is Relation-like [: the carrier of E,():] -defined [: the carrier of E,():] -valued Element of bool [:[: the carrier of E,():],[: the carrier of E,():]:]
F2 is set
TS1 is set
[F2,TS1] is V26() set
{F2,TS1} is non empty set
{F2} is non empty trivial V39(1) set
{{F2,TS1},{F2}} is non empty set
TS2 is set
y is set
[TS2,y] is V26() set
{TS2,y} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,y},{TS2}} is non empty set

[[F2,TS1],[TS2,y]] is V26() set
{[F2,TS1],[TS2,y]} is non empty Relation-like set
{[F2,TS1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[F2,TS1],[TS2,y]},{[F2,TS1]}} is non empty set
q is set
p is set
[q,p] is V26() set
{q,p} is non empty set
{q} is non empty trivial V39(1) set
{{q,p},{q}} is non empty set
v is set
v is set
[v,v] is V26() set
{v,v} is non empty set
{v} is non empty trivial V39(1) set
{{v,v},{v}} is non empty set
F2 is set
TS1 is set
[F2,TS1] is V26() set
{F2,TS1} is non empty set
{F2} is non empty trivial V39(1) set
{{F2,TS1},{F2}} is non empty set
TS2 is set
y is set
[TS2,y] is V26() set
{TS2,y} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,y},{TS2}} is non empty set
[[F2,TS1],[TS2,y]] is V26() set
{[F2,TS1],[TS2,y]} is non empty Relation-like set
{[F2,TS1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[F2,TS1],[TS2,y]},{[F2,TS1]}} is non empty set
q is set
p is set
q is set
p is set
[q,p] is V26() set
{q,p} is non empty set
{q} is non empty trivial V39(1) set
{{q,p},{q}} is non empty set
[q,p] is V26() set
{q,p} is non empty set
{q} is non empty trivial V39(1) set
{{q,p},{q}} is non empty set
[[q,p],[q,p]] is V26() set
{[q,p],[q,p]} is non empty Relation-like set
{[q,p]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[q,p],[q,p]},{[q,p]}} is non empty set
F1 is Relation-like [: the carrier of E,():] -defined [: the carrier of E,():] -valued Element of bool [:[: the carrier of E,():],[: the carrier of E,():]:]
F2 is Relation-like [: the carrier of E,():] -defined [: the carrier of E,():] -valued Element of bool [:[: the carrier of E,():],[: the carrier of E,():]:]
TS1 is Element of [: the carrier of E,():]
y is set
q is set
[y,q] is V26() set
{y,q} is non empty set
{y} is non empty trivial V39(1) set
{{y,q},{y}} is non empty set
TS2 is Element of [: the carrier of E,():]
p is set
v is set
[p,v] is V26() set
{p,v} is non empty set
{p} is non empty trivial V39(1) set
{{p,v},{p}} is non empty set
[TS1,TS2] is V26() set
{TS1,TS2} is non empty set
{TS1} is non empty trivial V39(1) set
{{TS1,TS2},{TS1}} is non empty set
q is Element of the carrier of E

l is Element of the carrier of E

x is set
X is set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
F1 is functional Element of bool ()
F2 is non empty (F1)
(E,F1,F2) is Relation-like [: the carrier of F2,():] -defined [: the carrier of F2,():] -valued Element of bool [:[: the carrier of F2,():],[: the carrier of F2,():]:]
the carrier of F2 is non empty set
[: the carrier of F2,():] is non empty Relation-like set
[:[: the carrier of F2,():],[: the carrier of F2,():]:] is non empty Relation-like set
bool [:[: the carrier of F2,():],[: the carrier of F2,():]:] is non empty set
TS1 is set
TS2 is set
[TS1,TS2] is V26() set
{TS1,TS2} is non empty set
{TS1} is non empty trivial V39(1) set
{{TS1,TS2},{TS1}} is non empty set
y is set
q is set
[y,q] is V26() set
{y,q} is non empty set
{y} is non empty trivial V39(1) set
{{y,q},{y}} is non empty set
x is set
X is set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
E is set
F1 is set
[E,F1] is V26() set
{E,F1} is non empty set
{E} is non empty trivial V39(1) set
{{E,F1},{E}} is non empty set
[[x,X],[E,F1]] is V26() set
{[x,X],[E,F1]} is non empty Relation-like set
{[x,X]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,X],[E,F1]},{[x,X]}} is non empty set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is non empty (TS1)
(F2,TS1,TS2) is Relation-like [: the carrier of TS2,(F2 ^omega):] -defined [: the carrier of TS2,(F2 ^omega):] -valued Element of bool [:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:]
the carrier of TS2 is non empty set
[: the carrier of TS2,(F2 ^omega):] is non empty Relation-like set
[:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:] is non empty set
the of TS2 is Relation-like [: the carrier of TS2,TS1:] -defined the carrier of TS2 -valued Element of bool [:[: the carrier of TS2,TS1:], the carrier of TS2:]
[: the carrier of TS2,TS1:] is Relation-like set
[:[: the carrier of TS2,TS1:], the carrier of TS2:] is Relation-like set
bool [:[: the carrier of TS2,TS1:], the carrier of TS2:] is non empty set
proj1 the of TS2 is Relation-like set
proj1 (proj1 the of TS2) is set
proj2 the of TS2 is set
x is set
X is non empty set
X ^omega is non empty functional set
bool () is non empty set
E is functional Element of bool ()
F1 is non empty (E)
(X,E,F1) is Relation-like [: the carrier of F1,():] -defined [: the carrier of F1,():] -valued Element of bool [:[: the carrier of F1,():],[: the carrier of F1,():]:]
the carrier of F1 is non empty set
[: the carrier of F1,():] is non empty Relation-like set
[:[: the carrier of F1,():],[: the carrier of F1,():]:] is non empty Relation-like set
bool [:[: the carrier of F1,():],[: the carrier of F1,():]:] is non empty set
F2 is set
TS1 is set
[F2,TS1] is V26() set
{F2,TS1} is non empty set
{F2} is non empty trivial V39(1) set
{{F2,TS1},{F2}} is non empty set
TS2 is Element of the carrier of F1

[TS2,y] is V26() set
{TS2,y} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,y},{TS2}} is non empty set
q is Element of the carrier of F1

[q,p] is V26() set
{q,p} is non empty set
{q} is non empty trivial V39(1) set
{{q,p},{q}} is non empty set
x is non empty set
x ^omega is non empty functional set
bool () is non empty set
X is functional Element of bool ()
E is functional Element of bool ()
F1 is non empty (X)
the of F1 is Relation-like [: the carrier of F1,X:] -defined the carrier of F1 -valued Element of bool [:[: the carrier of F1,X:], the carrier of F1:]
the carrier of F1 is non empty set
[: the carrier of F1,X:] is Relation-like set
[:[: the carrier of F1,X:], the carrier of F1:] is Relation-like set
bool [:[: the carrier of F1,X:], the carrier of F1:] is non empty set
(x,X,F1) is Relation-like [: the carrier of F1,():] -defined [: the carrier of F1,():] -valued Element of bool [:[: the carrier of F1,():],[: the carrier of F1,():]:]
[: the carrier of F1,():] is non empty Relation-like set
[:[: the carrier of F1,():],[: the carrier of F1,():]:] is non empty Relation-like set
bool [:[: the carrier of F1,():],[: the carrier of F1,():]:] is non empty set
F2 is non empty (E)
the of F2 is Relation-like [: the carrier of F2,E:] -defined the carrier of F2 -valued Element of bool [:[: the carrier of F2,E:], the carrier of F2:]
the carrier of F2 is non empty set
[: the carrier of F2,E:] is Relation-like set
[:[: the carrier of F2,E:], the carrier of F2:] is Relation-like set
bool [:[: the carrier of F2,E:], the carrier of F2:] is non empty set
(x,E,F2) is Relation-like [: the carrier of F2,():] -defined [: the carrier of F2,():] -valued Element of bool [:[: the carrier of F2,():],[: the carrier of F2,():]:]
[: the carrier of F2,():] is non empty Relation-like set
[:[: the carrier of F2,():],[: the carrier of F2,():]:] is non empty Relation-like set
bool [:[: the carrier of F2,():],[: the carrier of F2,():]:] is non empty set
TS1 is set
TS2 is Element of the carrier of F1

[TS2,q] is V26() set
{TS2,q} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,q},{TS2}} is non empty set
y is Element of the carrier of F1

[y,p] is V26() set
{y,p} is non empty set
{y} is non empty trivial V39(1) set
{{y,p},{y}} is non empty set
[[TS2,q],[y,p]] is V26() set
{[TS2,q],[y,p]} is non empty Relation-like set
{[TS2,q]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[TS2,q],[y,p]},{[TS2,q]}} is non empty set
TS1 is set
TS2 is Element of the carrier of F2

[TS2,q] is V26() set
{TS2,q} is non empty set
{TS2} is non empty trivial V39(1) set
{{TS2,q},{TS2}} is non empty set
y is Element of the carrier of F2

[y,p] is V26() set
{y,p} is non empty set
{y} is non empty trivial V39(1) set
{{y,p},{y}} is non empty set
[[TS2,q],[y,p]] is V26() set
{[TS2,q],[y,p]} is non empty Relation-like set
{[TS2,q]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[TS2,q],[y,p]},{[TS2,q]}} is non empty set
x is set
X is set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
E is set
F1 is set
[E,F1] is V26() set
{E,F1} is non empty set
{E} is non empty trivial V39(1) set
{{E,F1},{E}} is non empty set
[[x,X],[E,F1]] is V26() set
{[x,X],[E,F1]} is non empty Relation-like set
{[x,X]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,X],[E,F1]},{[x,X]}} is non empty set
F2 is non empty set
F2 ^omega is non empty functional set
bool (F2 ^omega) is non empty set
TS1 is functional Element of bool (F2 ^omega)
TS2 is non empty (TS1)
(F2,TS1,TS2) is Relation-like [: the carrier of TS2,(F2 ^omega):] -defined [: the carrier of TS2,(F2 ^omega):] -valued Element of bool [:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:]
the carrier of TS2 is non empty set
[: the carrier of TS2,(F2 ^omega):] is non empty Relation-like set
[:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:] is non empty Relation-like set
bool [:[: the carrier of TS2,(F2 ^omega):],[: the carrier of TS2,(F2 ^omega):]:] is non empty set
x is set
X is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set

[x,F1] is V26() set
{x,F1} is non empty set
{x} is non empty trivial V39(1) set
{{x,F1},{x}} is non empty set

[X,F2] is V26() set
{X,F2} is non empty set
{X} is non empty trivial V39(1) set
{{X,F2},{X}} is non empty set
[[x,F1],[X,F2]] is V26() set
{[x,F1],[X,F2]} is non empty Relation-like set
{[x,F1]} is non empty trivial Relation-like Function-like constant V39(1) set
{{[x,F1],[X,F2]},{[x,F1]}} is non empty set
TS1 is functional Element of bool ()
TS2 is non empty (TS1)
(E,TS1,TS2) is Relation-like [: the carrier of TS2,():] -defined [: the carrier of TS2,():] -valued Element of bool [:[: the carrier of TS2,():],[: the carrier of TS2,():]:]
the carrier of TS2 is non empty set
[: the carrier of TS2,():] is non empty Relation-like set
[:[: the carrier of TS2,():],[: the carrier of TS2,():]:] is non empty Relation-like set
bool [:[: the carrier of TS2,():],[: the carrier of TS2,():]:] is non empty set
x is set
X is set
[x,X] is V26() set
{x,X} is non empty set
{x} is non empty trivial V39(1) set
{{x,X},{x}} is non empty set
E is set
F1 is non empty set
F1 ^omega is non empty functional set
bool (F1 ^omega) is non empty set

K266(F1) is non empty functional M12(F1)
[E,(<%> F1)] is V26() set
{E,(<%> F1)} is non empty set
{E} is non empty trivial V39(1) set
{{E,(<%> F1)},{E}} is non