:: EQREL_1 semantic presentation

REAL is set
NAT is non empty V30() V31() V32() Element of bool REAL
bool REAL is non empty set
NAT is non empty V30() V31() V32() set
bool NAT is non empty set
bool NAT is non empty set

1 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
{{},1} is non empty set
2 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
3 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
X is set
(X) is Relation-like X -defined X -valued Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
dom (X) is Element of bool X
bool X is non empty set
P is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
P is set
field (X) is set
proj1 (X) is set
proj2 (X) is set
(proj1 (X)) \/ (proj2 (X)) is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
rng (X) is Element of bool X
(dom (X)) \/ (rng (X)) is Element of bool X
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(X) is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]

(X,(X),P) is Relation-like X -defined X -valued Element of bool [:X,X:]
X is set

[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
P is set
x is set
a is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
X is set

[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
X is set
(X) is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
P is set
x is set
a is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
field (X) is set
proj1 (X) is set
proj2 (X) is set
(proj1 (X)) \/ (proj2 (X)) is set
X is set
(X) is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
X is set
P is set
[X,P] is non empty V38() set
{X,P} is non empty set
{X} is non empty trivial set
{{X,P},{X}} is non empty set
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set

dom a is Element of bool x
bool x is non empty set
rng a is Element of bool x
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
x is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]
field x is set
proj1 x is set
proj2 x is set
() \/ () is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
a is Relation-like X -defined X -valued symmetric total V41(X,X) Element of bool [:X,X:]
field a is set
proj1 a is set
proj2 a is set
() \/ () is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
a is set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set

field b is set
proj1 b is set
proj2 b is set
() \/ () is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
x is set
P is Relation-like X -defined X -valued reflexive total V41(X,X) Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

field P is set
proj1 P is set
proj2 P is set
() \/ () is set
dom P is Element of bool X
bool X is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

a is set
[a,a] is non empty V38() set
{a,a} is non empty set
{a} is non empty trivial set
{{a,a},{a}} is non empty set

a is set
[a,a] is non empty V38() set
{a,a} is non empty set
{a} is non empty trivial set
{{a,a},{a}} is non empty set

dom (X,P,x) is Element of bool X
bool X is non empty set
rng (X,P,x) is Element of bool X
field (X,P,x) is set
proj1 (X,P,x) is set
proj2 (X,P,x) is set
(proj1 (X,P,x)) \/ (proj2 (X,P,x)) is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,(id X),P) is Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive total V41(X,X) Element of bool [:X,X:]
x is set
a is set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
bool (bool [:X,X:]) is non empty set
P is Element of bool (bool [:X,X:])

a is set
b is set
[a,b] is non empty V38() set
{a,b} is non empty set
{a} is non empty trivial set
{{a,b},{a}} is non empty set
[b,a] is non empty V38() set
{b,a} is non empty set
{b} is non empty trivial set
{{b,a},{b}} is non empty set
c is set
a is set
b is set
[a,b] is non empty V38() set
{a,b} is non empty set
{a} is non empty trivial set
{{a,b},{a}} is non empty set
c is set
[b,c] is non empty V38() set
{b,c} is non empty set
{b} is non empty trivial set
{{b,c},{b}} is non empty set
[a,c] is non empty V38() set
{a,c} is non empty set
{{a,c},{a}} is non empty set
B is set
a is set
[a,a] is non empty V38() set
{a,a} is non empty set
{a} is non empty trivial set
{{a,a},{a}} is non empty set
b is set
field x is set
proj1 x is set
proj2 x is set
() \/ () is set
dom x is Element of bool X
bool X is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

bool (bool [:X,X:]) is non empty set
x is Element of bool (bool [:X,X:])

a is set

b is set

X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]

(X,b,c) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]

(X,c,b) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]

(X,a,a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]

(X,b,b) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]

X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P,x) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]

(X,(X,P,x),a) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,x,a) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,(X,x,a)) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]

(X,x,a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,P,(X,x,a)) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,(X,P,x),a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]

(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,(X,P,x),a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,x,a) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
(X,P,(X,x,a)) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P,P) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P,x) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,x,P) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P,x) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,(X,P,x)) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P,x) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,(X,P,x)) is Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]
(X,P,(X,P,x)) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]

F1() is set
[:F1(),F1():] is Relation-like set
bool [:F1(),F1():] is non empty set
X is Relation-like F1() -defined F1() -valued Element of bool [:F1(),F1():]
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
a is set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
P is set
[P,P] is non empty V38() set
{P,P} is non empty set
{P} is non empty trivial set
{{P,P},{P}} is non empty set
field X is set
proj1 X is set
proj2 X is set
() \/ () is set
dom X is Element of bool F1()
bool F1() is non empty set
P is Relation-like F1() -defined F1() -valued reflexive symmetric transitive total V41(F1(),F1()) Element of bool [:F1(),F1():]
x is set
a is set
[x,a] is non empty V38() set
{x,a} is non empty set
{x} is non empty trivial set
{{x,a},{x}} is non empty set
b is set
c is set
[b,c] is non empty V38() set
{b,c} is non empty set
{b} is non empty trivial set
{{b,c},{b}} is non empty set
X is set
P is set
[:X,P:] is Relation-like set
bool [:X,P:] is non empty set

a is set
Im (x,a) is set
{a} is non empty trivial set
x .: {a} is set
bool P is non empty set
x .: {a} is Element of bool P
X is set
P is set
[P,X] is non empty V38() set
{P,X} is non empty set
{P} is non empty trivial set
{{P,X},{P}} is non empty set

Im (x,P) is set
x .: {P} is set
a is set
[a,X] is non empty V38() set
{a,X} is non empty set
{a} is non empty trivial set
{{a,X},{a}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
[P,x] is non empty V38() set
{P,x} is non empty set
{P} is non empty trivial set
{{P,x},{P}} is non empty set
a is Relation-like X -defined X -valued symmetric total V41(X,X) Element of bool [:X,X:]
(X,X,a,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
a .: {x} is set
[x,P] is non empty V38() set
{x,P} is non empty set
{{x,P},{x}} is non empty set
b is set
[b,P] is non empty V38() set
{b,P} is non empty set
{b} is non empty trivial set
{{b,P},{b}} is non empty set
[x,P] is non empty V38() set
{x,P} is non empty set
{{x,P},{x}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

x is set
(X,X,P,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
P .: {x} is set
[x,x] is non empty V38() set
{x,x} is non empty set
{{x,x},{x}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

x is set
(X,X,P,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
P .: {x} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
x is set
a is set
[P,a] is non empty V38() set
{P,a} is non empty set
{P} is non empty trivial set
{{P,a},{P}} is non empty set

(X,X,b,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
b .: {x} is set
[a,x] is non empty V38() set
{a,x} is non empty set
{a} is non empty trivial set
{{a,x},{a}} is non empty set
[x,a] is non empty V38() set
{x,a} is non empty set
{{x,a},{x}} is non empty set
[P,x] is non empty V38() set
{P,x} is non empty set
{{P,x},{P}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set

(X,X,x,P) is Element of bool X
bool X is non empty set
{P} is non empty trivial set
x .: {P} is set
a is set
[a,P] is non empty V38() set
{a,P} is non empty set
{a} is non empty trivial set
{{a,P},{a}} is non empty set
(X,X,x,a) is Element of bool X
x .: {a} is set
b is set
[b,P] is non empty V38() set
{b,P} is non empty set
{b} is non empty trivial set
{{b,P},{b}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
[b,a] is non empty V38() set
{b,a} is non empty set
{{b,a},{b}} is non empty set
b is set
[b,a] is non empty V38() set
{b,a} is non empty set
{b} is non empty trivial set
{{b,a},{b}} is non empty set
[b,P] is non empty V38() set
{b,P} is non empty set
{{b,P},{b}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set

(X,X,x,P) is Element of bool X
bool X is non empty set
{P} is non empty trivial set
x .: {P} is set
a is set
(X,X,x,a) is Element of bool X
{a} is non empty trivial set
x .: {a} is set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
[a,P] is non empty V38() set
{a,P} is non empty set
{{a,P},{a}} is non empty set
[a,P] is non empty V38() set
{a,P} is non empty set
{{a,P},{a}} is non empty set
[P,a] is non empty V38() set
{P,a} is non empty set
{{P,a},{P}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

x is set
(X,X,P,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
P .: {x} is set
a is set
(X,X,P,a) is Element of bool X
{a} is non empty trivial set
P .: {a} is set
[x,a] is non empty V38() set
{x,a} is non empty set
{{x,a},{x}} is non empty set
b is set
[b,x] is non empty V38() set
{b,x} is non empty set
{b} is non empty trivial set
{{b,x},{b}} is non empty set
[x,b] is non empty V38() set
{x,b} is non empty set
{{x,b},{x}} is non empty set
[b,a] is non empty V38() set
{b,a} is non empty set
{{b,a},{b}} is non empty set
X is set

[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
(X,X,(id X),P) is Element of bool X
bool X is non empty set
{P} is non empty trivial set
(id X) .: {P} is set
x is set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
x is set
a is set
X is set

[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is set
(X,X,(X),P) is Element of bool X
bool X is non empty set
{P} is non empty trivial set
(X) .: {P} is set
x is set
[x,P] is non empty V38() set
{x,P} is non empty set
{x} is non empty trivial set
{{x,P},{x}} is non empty set
x is set
a is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

x is set
(X,X,P,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial set
P .: {x} is set
a is set
b is set
[a,b] is non empty V38() set
{a,b} is non empty set
{a} is non empty trivial set
{{a,b},{a}} is non empty set
[b,x] is non empty V38() set
{b,x} is non empty set
{b} is non empty trivial set
{{b,x},{b}} is non empty set
[x,b] is non empty V38() set
{x,b} is non empty set
{{x,b},{x}} is non empty set
[a,x] is non empty V38() set
{a,x} is non empty set
{{a,x},{a}} is non empty set
X is set
P is set
[:P,P:] is Relation-like set
bool [:P,P:] is non empty set
x is set
[X,x] is non empty V38() set
{X,x} is non empty set
{X} is non empty trivial set
{{X,x},{X}} is non empty set

(P,a,b) is Relation-like P -defined P -valued reflexive symmetric transitive total V41(P,P) Element of bool [:P,P:]
(P,a,b) is Relation-like P -defined P -valued reflexive symmetric Element of bool [:P,P:]

B is set
u is set
[B,u] is non empty V38() set
{B,u} is non empty set
{B} is non empty trivial set
{{B,u},{B}} is non empty set
X1 is set
[u,X1] is non empty V38() set
{u,X1} is non empty set
{u} is non empty trivial set
{{u,X1},{u}} is non empty set
[B,X1] is non empty V38() set
{B,X1} is non empty set
{{B,X1},{B}} is non empty set

len Y1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . 1 is set
Y1 . (len Y1) is set

len y is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
y . 1 is set
y . (len y) is set

len (y ^ Y1) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(len y) + (len Y1) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(len y) + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(y ^ Y1) . (len (y ^ Y1)) is set
(len Y1) + (len y) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
((len Y1) + (len y)) - (len y) is ext-real V29() V37() set
Y1 . (((len Y1) + (len y)) - (len y)) is set
A is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(y ^ Y1) . A is set
A + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(y ^ Y1) . (A + 1) is set
[((y ^ Y1) . A),((y ^ Y1) . (A + 1))] is non empty V38() set
{((y ^ Y1) . A),((y ^ Y1) . (A + 1))} is non empty set
{((y ^ Y1) . A)} is non empty trivial set
{{((y ^ Y1) . A),((y ^ Y1) . (A + 1))},{((y ^ Y1) . A)}} is non empty set
Seg (len y) is V44() V51( len y) Element of bool NAT
dom y is Element of bool NAT
y . (A + 1) is set
y . A is set
Seg (len y) is V44() V51( len y) Element of bool NAT
dom y is Element of bool NAT
[u,u] is non empty V38() set
{u,u} is non empty set
{{u,u},{u}} is non empty set
1 + (len y) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(1 + (len y)) - (len y) is ext-real V29() V37() set
Y1 . ((1 + (len y)) - (len y)) is set
A - (len y) is ext-real V29() V37() set
1 + A is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(1 + A) - (len y) is ext-real V29() V37() set
Y1 . ((1 + A) - (len y)) is set
(A - (len y)) + 1 is ext-real V29() V37() set
Y1 . ((A - (len y)) + 1) is set
1 + (len y) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(1 + (len y)) - (len y) is ext-real V29() V37() set
T is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . T is set
T + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . (T + 1) is set
[(Y1 . T),(Y1 . (T + 1))] is non empty V38() set
{(Y1 . T),(Y1 . (T + 1))} is non empty set
{(Y1 . T)} is non empty trivial set
{{(Y1 . T),(Y1 . (T + 1))},{(Y1 . T)}} is non empty set
Seg (len y) is V44() V51( len y) Element of bool NAT
dom y is Element of bool NAT
(y ^ Y1) . 1 is set
B is set
u is set
[B,u] is non empty V38() set
{B,u} is non empty set
{B} is non empty trivial set
{{B,u},{B}} is non empty set
[u,B] is non empty V38() set
{u,B} is non empty set
{u} is non empty trivial set
{{u,B},{u}} is non empty set

len X1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
X1 . 1 is set
X1 . (len X1) is set
1 + (len X1) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Seg (len X1) is V44() V51( len X1) Element of bool NAT
Y1 is ext-real V29() V30() V31() V32() V36() V37() set
(1 + (len X1)) - Y1 is ext-real V29() V37() set
X1 . ((1 + (len X1)) - Y1) is set

dom Y1 is Element of bool NAT
len Y1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
y is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . y is set
y + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
Y1 . (y + 1) is set
[(Y1 . y),(Y1 . (y + 1))] is non empty V38() set
{(Y1 . y),(Y1 . (y + 1))} is non empty set
{(Y1 . y)} is non empty trivial set
{{(Y1 . y),(Y1 . (y + 1))},{(Y1 . y)}} is non empty set
(len X1) - y is ext-real V29() V37() set
(len X1) - (len X1) is ext-real V29() V37() set
y - (len X1) is ext-real V29() V37() set

- ((len X1) - y) is ext-real V29() V37() set
c is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
0 + 1 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
- y is ext-real V29() V37() set
0 + (len X1) is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
(len X1) + (- y) is ext-real V29() V37() set
X1 . c is set
c + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
X1 . (c + 1) is set
[(X1 . c),(X1 . (c + 1))] is non empty V38() set
{(X1 . c),(X1 . (c + 1))} is non empty set
{(X1 . c)} is non empty trivial set
{{(X1 . c),(X1 . (c + 1))},{(X1 . c)}} is non empty set
[(X1 . (c + 1)),(X1 . c)] is non empty V38() set
{(X1 . (c + 1)),(X1 . c)} is non empty set
{(X1 . (c + 1))} is non empty trivial set
{{(X1 . (c + 1)),(X1 . c)},{(X1 . (c + 1))}} is non empty set
[(X1 . (c + 1)),(X1 . c)] is non empty V38() set
{(X1 . (c + 1)),(X1 . c)} is non empty set
{(X1 . (c + 1))} is non empty trivial set
{{(X1 . (c + 1)),(X1 . c)},{(X1 . (c + 1))}} is non empty set
[(X1 . (c + 1)),(X1 . c)] is non empty V38() set
{(X1 . (c + 1)),(X1 . c)} is non empty set
{(X1 . (c + 1))} is non empty trivial set
{{(X1 . (c + 1)),(X1 . c)},{(X1 . (c + 1))}} is non empty set
[(X1 . (c + 1)),(X1 . c)] is non empty V38() set
{(X1 . (c + 1)),(X1 . c)} is non empty set
{(X1 . (c + 1))} is non empty trivial set
{{(X1 . (c + 1)),(X1 . c)},{(X1 . (c + 1))}} is non empty set
(len X1) + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
1 + y is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
((len X1) + 1) - (1 + y) is ext-real V29() V37() set
X1 . (((len X1) + 1) - (1 + y)) is set
X1 . ((len X1) - y) is set
(1 + (len X1)) - y is ext-real V29() V37() set
X1 . ((1 + (len X1)) - y) is set
((len X1) - y) + 1 is ext-real V29() V37() set
X1 . (((len X1) - y) + 1) is set
Y1 . (len X1) is set
(1 + (len X1)) - (len X1) is ext-real V29() V37() set
X1 . ((1 + (len X1)) - (len X1)) is set

1 + 0 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
X1 . (1 + 0) is set
Y1 . (len Y1) is set
Y1 . 1 is set
(len X1) + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
((len X1) + 1) - 1 is ext-real V29() V37() set
X1 . (((len X1) + 1) - 1) is set
B is set
[B,B] is non empty V38() set
{B,B} is non empty set
{B} is non empty trivial set
{{B,B},{B}} is non empty set

len <*B*> is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
X1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
<*B*> . X1 is set
X1 + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
<*B*> . (X1 + 1) is set
[(<*B*> . X1),(<*B*> . (X1 + 1))] is non empty V38() set
{(<*B*> . X1),(<*B*> . (X1 + 1))} is non empty set
{(<*B*> . X1)} is non empty trivial set
{{(<*B*> . X1),(<*B*> . (X1 + 1))},{(<*B*> . X1)}} is non empty set
<*B*> . 1 is set
field c is set
proj1 c is set
proj2 c is set
() \/ () is set
dom c is Element of bool P
bool P is non empty set

u is set
X1 is set
[u,X1] is non empty V38() set
{u,X1} is non empty set
{u} is non empty trivial set
{{u,X1},{u}} is non empty set

len <*u,X1*> is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
1 + 1 is non empty ext-real positive non negative V29() V30() V31() V32() V36() V37() Element of NAT
<*u,X1*> . 1 is set
y is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
<*u,X1*> . y is set
y + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
<*u,X1*> . (y + 1) is set
[(<*u,X1*> . y),(<*u,X1*> . (y + 1))] is non empty V38() set
{(<*u,X1*> . y),(<*u,X1*> . (y + 1))} is non empty set
{(<*u,X1*> . y)} is non empty trivial set
{{(<*u,X1*> . y),(<*u,X1*> . (y + 1))},{(<*u,X1*> . y)}} is non empty set
<*u,X1*> . (len <*u,X1*>) is set

len u is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
u . 1 is set
u . (len u) is set
X1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
u . X1 is set
X1 + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
u . (X1 + 1) is set
[(u . X1),(u . (X1 + 1))] is non empty V38() set
{(u . X1),(u . (X1 + 1))} is non empty set
{(u . X1)} is non empty trivial set
{{(u . X1),(u . (X1 + 1))},{(u . X1)}} is non empty set

len c is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
c . 1 is set
c . (len c) is set
B is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
c . B is set
[(c . 1),(c . B)] is non empty V38() set
{(c . 1),(c . B)} is non empty set
{(c . 1)} is non empty trivial set
{{(c . 1),(c . B)},{(c . 1)}} is non empty set
B + 1 is ext-real V29() V30() V31() V32() V36() V37() Element of NAT
c . (B + 1) is set
[(c . 1),(c . (B + 1))] is non empty V38() set
{(c . 1),(c . (B + 1))} is non empty set
{{(c . 1),(c . (B + 1))},{(c . 1)}} is non empty set
[(c . B),(c . (B + 1))] is non empty V38() set
{(c . B),(c . (B + 1))} is non empty set
{(c . B)} is non empty trivial set
{{(c . B),(c . (B + 1))},{(c . B)}} is non empty set

[(c . 1),(c . 1)] is non empty V38() set
{(c . 1),(c . 1)} is non empty set
{{(c . 1),(c . 1)},{(c . 1)}} is non empty set

c . 0 is set
[(c . 1),(c . 0)] is non empty V38() set
{(c . 1),(c . 0)} is non empty set
{{(c . 1),(c . 0)},{(c . 1)}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]

b is set
(X,X,a,b) is Element of bool X
bool X is non empty set
{b} is non empty trivial set
a .: {b} is set
(X,X,P,b) is Element of bool X
P .: {b} is set
(X,X,x,b) is Element of bool X
x .: {b} is set
c is set
[c,b] is non empty V38() set
{c,b} is non empty set
{c} is non empty trivial set
{{c,b},{c}} is non empty set
B is set
[B,b] is non empty V38() set
{B,b} is non empty set
{B} is non empty trivial set
{{B,b},{B}} is non empty set
[c,B] is non empty V38() set
{c,B} is non empty set
{{c,B},{c}} is non empty set
[B,c] is non empty V38() set
{B,c} is non empty set
{{B,c},{B}} is non empty set
[b,B] is non empty V38() set
{b,B} is non empty set
{{b,B},{b}} is non empty set
[b,c] is non empty V38() set
{b,c} is non empty set
{{b,c},{b}} is non empty set
b is set
(X,X,a,b) is Element of bool X
bool X is non empty set
{b} is non empty trivial set
a .: {b} is set
(X,X,P,b) is Element of bool X
P .: {b} is set
(X,X,x,b) is Element of bool X
x .: {b} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P,x) is Relation-like X -defined X -valued reflexive symmetric Element of bool [:X,X:]
the Element of X is Element of X
b is set
(X,X,(X),b) is Element of bool X
bool X is non empty set
{b} is non empty trivial set
(X) .: {b} is set
(X,X,P,b) is Element of bool X
P .: {b} is set
(X,X,x,b) is Element of bool X
x .: {b} is set
(X,X,P, the Element of X) is Element of bool X
{ the Element of X} is non empty trivial set
P .: { the Element of X} is set
(X,X,x, the Element of X) is Element of bool X
x .: { the Element of X} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
bool X is non empty set
bool (bool X) is non empty set

x is Element of bool (bool X)
a is Element of bool X
c is set
b is Element of bool X
(X,X,P,c) is Element of bool X
{c} is non empty trivial set
P .: {c} is set
x is Element of bool (bool X)
a is Element of bool (bool X)
b is Element of bool X
c is set
(X,X,P,c) is Element of bool X
{c} is non empty trivial set
P .: {c} is set
c is set
(X,X,P,c) is Element of bool X
{c} is non empty trivial set
P .: {c} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
the Element of (X,P) is Element of (X,P)
a is set
(X,X,P,a) is Element of bool X
{a} is non empty trivial set
P .: {a} is set
X is set
bool X is non empty set
bool (bool X) is non empty set
P is Element of bool (bool X)
x is Element of bool X
a is set
{a} is non empty trivial set
b is Element of bool X
c is set
{c} is non empty trivial set
B is set
union P is Element of bool X
x is set
{x} is non empty trivial set
a is set
b is set
x is Element of bool X
a is Element of bool X
X is ( {} )
P is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
x is set
(X,X,P,x) is Element of bool X
{x} is non empty trivial set
P .: {x} is set
a is set
a is set
b is set
union (X,P) is Element of bool X
x is Element of bool X
a is set
(X,X,P,a) is Element of bool X
{a} is non empty trivial set
P .: {a} is set
a is Element of bool X
b is set
(X,X,P,b) is Element of bool X
{b} is non empty trivial set
P .: {b} is set
c is set
(X,X,P,c) is Element of bool X
{c} is non empty trivial set
P .: {c} is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
P is (X)
bool X is non empty set
x is set
a is set
b is set
c is Element of bool X
B is Element of bool X
union P is Element of bool X
x is set
a is set
b is Element of bool X
b is Element of bool X
x is set
a is set

(X,x) is Element of bool (bool X)
bool (bool X) is non empty set
a is Element of bool X
the Element of a is Element of a
c is set
(X,X,x, the Element of a) is Element of bool X
{ the Element of a} is non empty trivial set
x .: { the Element of a} is set
[c, the Element of a] is non empty V38() set
{c, the Element of a} is non empty set
{c} is non empty trivial set
{{c, the Element of a},{c}} is non empty set
B is Element of bool X
b is set
(X,X,x,b) is Element of bool X
{b} is non empty trivial set
x .: {b} is set
[b,b] is non empty V38() set
{b,b} is non empty set
{{b,b},{b}} is non empty set
c is Element of bool X
B is set
[B,b] is non empty V38() set
{B,b} is non empty set
{B} is non empty trivial set
{{B,b},{B}} is non empty set
u is Element of bool X

(X, the Relation-like X -defined X -valued reflexive symmetric transitive total V41(X,X) Element of bool [:X,X:]) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set

(X,x) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set

(X,a) is Element of bool (bool X)
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
a is set
P is set
[a,P] is non empty V38() set
{a,P} is non empty set
{a} is non empty trivial set
{{a,P},{a}} is non empty set

(X,X,x,a) is Element of bool X
bool X is non empty set
x .: {a} is set
(X,X,x,P) is Element of bool X
{P} is non empty trivial set
x .: {P} is set
X is set
P is set
[:P,P:] is Relation-like set
bool [:P,P:] is non empty set

(P,x) is Element of bool (bool P)
bool P is non empty set
bool (bool P) is non empty set
a is Element of bool P
b is set
(P,P,x,b) is Element of bool P
{b} is non empty trivial set
x .: {b} is set
c is Element of P
(P,P,x,c) is Element of bool P
{c} is non empty trivial set
x .: {c} is set
X is non empty set
the Element of X is Element of X
x is (X)
union x is Element of bool X
bool X is non empty set
a is set
X is set
P is (X)
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set

(X,P) is Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set

(X,P) is non empty with_non-empty_elements (X)
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set

(X,P) is non empty with_non-empty_elements (X)
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set

x is Element of X
Im (P,x) is set
{x} is non empty trivial set
P .: {x} is set
bool X is non empty set
(X,P) is non empty with_non-empty_elements (X)
(X,X,P,x) is Element of bool X
X is set

[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(X,(id X)) is with_non-empty_elements (X)
X is non empty set
(X) is non empty with_non-empty_elements (X)

[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
(X,(id X)) is non empty with_non-empty_elements (X)
{ {b1} where b1 is Element of X : verum } is set
x is set
a is set
(X,X,(id X),a) is Element of bool X
bool X is non empty set
{a} is non empty trivial set
(id X) .: {a} is set
x is set
a is Element of X
{a} is non empty trivial Element of bool X
(X,X,(id X),a) is Element of bool X
{a} is non empty trivial set
(id X) .: {a} is set
X is non empty set
bool X is non empty set
P is Element of X
x is non empty with_non-empty_elements (X)
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set

(X,a) is non empty with_non-empty_elements (X)
(X,X,a,P) is Element of bool X
{P} is non empty trivial set
a .: {P} is set
a is