:: REWRITE1 semantic presentation

REAL is set
NAT is non empty V23() V24() V25() V51() V56() V57() Element of K10(REAL)
K10(REAL) is set
NAT is non empty V23() V24() V25() V51() V56() V57() set
K10(NAT) is V51() set
K10(NAT) is V51() set
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
3 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
field {} is set
dom {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
rng {} is empty V2() V4() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
(dom {}) \/ (rng {}) is Relation-like set
Seg 1 is non empty V2() V51() V58(1) Element of K10(NAT)
{1} is non empty V2() V58(1) set
Seg 2 is non empty V51() V58(2) Element of K10(NAT)
{1,2} is non empty set
len {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
R ^ C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
0 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set
1 + a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Seg b is V51() V58(b) Element of K10(NAT)
R | (Seg b) is Relation-like NAT -defined Seg b -defined NAT -defined Function-like FinSubsequence-like set
x2 is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
x2 ^ C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
P is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
Seg X is V51() V58(X) Element of K10(NAT)
R | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined Function-like FinSubsequence-like set
x2 is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
P ^ C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
P is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
P + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
Seg P is V51() V58(P) Element of K10(NAT)
R | (Seg P) is Relation-like NAT -defined Seg P -defined NAT -defined Function-like FinSubsequence-like set
Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
a ^ C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
dom R is Element of K10(NAT)
len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Seg (len R) is V51() V58( len R) Element of K10(NAT)
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
0 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set
C + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
dom R is Element of K10(NAT)
len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Seg (len R) is V51() V58( len R) Element of K10(NAT)
dom R is Element of K10(NAT)
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set
C + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
dom R is Element of K10(NAT)
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
({},R) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
(R,{}) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
{} ^ R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
R ^ {} is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
C ^ R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
a is set
<*a*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
C ^ <*a*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
((C ^ <*a*>),R) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len <*a*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
len (C ^ <*a*>) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
len C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len C) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
Seg b is V51() V58(b) Element of K10(NAT)
(C ^ <*a*>) | (Seg b) is Relation-like NAT -defined Seg b -defined NAT -defined Function-like FinSubsequence-like set
x2 ^ R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
x2 ^ Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
C ^ Q is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
(len x2) + 0 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
len Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len C) + (len Q) is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
a is set
<*a*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
R ^ <*a*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
b is set
<*b*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
<*b*> ^ C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
((R ^ <*a*>),(<*b*> ^ C)) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
R ^ <*b*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
(R ^ <*b*>) ^ C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
R ^ (<*b*> ^ C) is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
C is set
<*C*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
(<*C*>,R) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
{} ^ <*C*> is non empty Relation-like NAT -defined Function-like V51() V58({} + 1) FinSequence-like FinSubsequence-like set
{} + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
{} ^ R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
x2 is set
<*x2*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
b ^ <*x2*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
len <*x2*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len b) + (len <*x2*>) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
<*x2*> ^ {} is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
Q is set
<*Q*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
X is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
<*Q*> ^ X is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len X) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
X ^ <*x2*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len (X ^ <*x2*>) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
<*Q*> ^ (X ^ <*x2*>) is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len C is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
F₁() is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
dom F₁() is Element of K10(NAT)
F₂() is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
dom F₂() is Element of K10(NAT)
len F₁() is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
len F₂() is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
F₁() . (len F₁()) is set
F₂() . 1 is set
(F₁(),F₂()) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
dom (F₁(),F₂()) is Element of K10(NAT)
R is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
C is set
<*C*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
R ^ <*C*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
R ^ F₂() is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
Seg (len F₂()) is V51() V58( len F₂()) Element of K10(NAT)
a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(F₁(),F₂()) . a is set
(F₁(),F₂()) . (a + 1) is set
b is set
x2 is set
len R is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
len <*C*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len R) + (len <*C*>) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len R) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
F₁() . a is set
F₁() . (a + 1) is set
Seg (len R) is V51() V58( len R) Element of K10(NAT)
dom R is Element of K10(NAT)
R . (a + 1) is set
R . a is set
Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set
(len F₁()) + Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
1 + X is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len R) + (1 + X) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
len (F₁(),F₂()) is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len R) + (len F₂()) is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(X + 1) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
F₂() . (X + 1) is set
((len R) + (1 + X)) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len R) + ((X + 1) + 1) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
F₂() . ((X + 1) + 1) is set
R is Relation-like set
<*{}*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
C is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
len C is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
dom C is non empty V2() V58(1) Element of K10(NAT)
a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . a is set
C . (a + 1) is set
[(C . a),(C . (a + 1))] is set
{(C . a),(C . (a + 1))} is non empty set
{(C . a)} is non empty V2() V58(1) set
{{(C . a),(C . (a + 1))},{(C . a)}} is non empty set
R is Relation-like set
C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
R is Relation-like set
C is set
<*C*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
len <*C*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
dom <*C*> is non empty V2() V58(1) Element of K10(NAT)
b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
<*C*> . b is set
<*C*> . (b + 1) is set
[(<*C*> . b),(<*C*> . (b + 1))] is set
{(<*C*> . b),(<*C*> . (b + 1))} is non empty set
{(<*C*> . b)} is non empty V2() V58(1) set
{{(<*C*> . b),(<*C*> . (b + 1))},{(<*C*> . b)}} is non empty set
R is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
<*C,a*> is non empty Relation-like NAT -defined Function-like V51() V58(2) FinSequence-like FinSubsequence-like set
len <*C,a*> is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
dom <*C,a*> is non empty V58(2) Element of K10(NAT)
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
<*C,a*> . x2 is set
<*C,a*> . (x2 + 1) is set
[(<*C,a*> . x2),(<*C,a*> . (x2 + 1))] is set
{(<*C,a*> . x2),(<*C,a*> . (x2 + 1))} is non empty set
{(<*C,a*> . x2)} is non empty V2() V58(1) set
{{(<*C,a*> . x2),(<*C,a*> . (x2 + 1))},{(<*C,a*> . x2)}} is non empty set
1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
<*C,a*> . 1 is set
R is Relation-like set
C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
len C is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . (len C) is set
a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
a . 1 is set
(C,a) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
x2 is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
Q is set
<*Q*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
x2 ^ <*Q*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 ^ a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len (C,a) is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
dom (C,a) is Element of K10(NAT)
dom a is non empty Element of K10(NAT)
X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a . X is set
a . (X + 1) is set
[(a . X),(a . (X + 1))] is set
{(a . X),(a . (X + 1))} is non empty set
{(a . X)} is non empty V2() V58(1) set
{{(a . X),(a . (X + 1))},{(a . X)}} is non empty set
dom C is non empty Element of K10(NAT)
X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . X is set
C . (X + 1) is set
[(C . X),(C . (X + 1))] is set
{(C . X),(C . (X + 1))} is non empty set
{(C . X)} is non empty V2() V58(1) set
{{(C . X),(C . (X + 1))},{(C . X)}} is non empty set
X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(C,a) . X is set
(C,a) . (X + 1) is set
[((C,a) . X),((C,a) . (X + 1))] is set
{((C,a) . X),((C,a) . (X + 1))} is non empty set
{((C,a) . X)} is non empty V2() V58(1) set
{{((C,a) . X),((C,a) . (X + 1))},{((C,a) . X)}} is non empty set
R is Relation-like set
R ~ is Relation-like set
C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
Rev C is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len C is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
len (Rev C) is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
dom (Rev C) is Element of K10(NAT)
a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(Rev C) . a is set
(Rev C) . (a + 1) is set
[((Rev C) . a),((Rev C) . (a + 1))] is set
{((Rev C) . a),((Rev C) . (a + 1))} is non empty set
{((Rev C) . a)} is non empty V2() V58(1) set
{{((Rev C) . a),((Rev C) . (a + 1))},{((Rev C) . a)}} is non empty set
Seg (len C) is non empty V51() V58( len C) Element of K10(NAT)
(len C) - (a + 1) is ext-real V22() V30() set
((len C) - (a + 1)) + 1 is ext-real V22() V30() set
dom C is non empty Element of K10(NAT)
b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(len C) - a is ext-real V22() V30() set
b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . b is set
C . (b + 1) is set
[(C . b),(C . (b + 1))] is set
{(C . b),(C . (b + 1))} is non empty set
{(C . b)} is non empty V2() V58(1) set
{{(C . b),(C . (b + 1))},{(C . b)}} is non empty set
((len C) - a) + 1 is ext-real V22() V30() set
C . (((len C) - a) + 1) is set
C . (((len C) - (a + 1)) + 1) is set
R is Relation-like set
C is Relation-like set
a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
len a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
dom a is non empty Element of K10(NAT)
b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a . b is set
a . (b + 1) is set
[(a . b),(a . (b + 1))] is set
{(a . b),(a . (b + 1))} is non empty set
{(a . b)} is non empty V2() V58(1) set
{{(a . b),(a . (b + 1))},{(a . b)}} is non empty set
R is Relation-like set
C is set
a is set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
dom b is non empty Element of K10(NAT)
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
b . (x2 + 1) is set
[(b . x2),(b . (x2 + 1))] is set
{(b . x2),(b . (x2 + 1))} is non empty set
{(b . x2)} is non empty V2() V58(1) set
{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set
b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . 1 is set
b . (len b) is set
dom b is Element of K10(NAT)
x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
x2 . 1 is set
len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (len x2) is set
R is Relation-like set
C is set
<*C*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
a . 1 is set
len a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a . (len a) is set
R is set
C is set
a is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like ( {} )
a . 1 is set
len a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a . (len a) is set
dom a is non empty Element of K10(NAT)
1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
a is set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
dom b is non empty Element of K10(NAT)
1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (1 + 1) is set
[(b . 1),(b . (1 + 1))] is set
{(b . 1),(b . (1 + 1))} is non empty set
{(b . 1)} is non empty V2() V58(1) set
{{(b . 1),(b . (1 + 1))},{(b . 1)}} is non empty set
R is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
<*C,a*> is non empty Relation-like NAT -defined Function-like V51() V58(2) FinSequence-like FinSubsequence-like set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
R is Relation-like set
C is set
a is set
b is set
x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
x2 . 1 is set
len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (len x2) is set
Q is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
Q . 1 is set
len Q is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . (len Q) is set
(x2,Q) is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
X is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
X . 1 is set
len X is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
X . (len X) is set
P is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
P is set
<*P*> is non empty V2() Relation-like NAT -defined Function-like constant V51() V58(1) FinSequence-like FinSubsequence-like set
P ^ <*P*> is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
Seg (len Q) is non empty V51() V58( len Q) Element of K10(NAT)
dom Q is non empty Element of K10(NAT)
P ^ Q is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len P is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Seg (len P) is V51() V58( len P) Element of K10(NAT)
dom P is Element of K10(NAT)
P . 1 is set
(len P) + (len Q) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
R is Relation-like set
C is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
dom C is non empty Element of K10(NAT)
a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . a is set
C . b is set
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set
a + x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a + Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . (a + Q) is set
Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a + (Q + 1) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
(a + Q) + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
len C is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . (a + (Q + 1)) is set
[(C . (a + Q)),(C . (a + (Q + 1)))] is set
{(C . (a + Q)),(C . (a + (Q + 1)))} is non empty set
{(C . (a + Q))} is non empty V2() V58(1) set
{{(C . (a + Q)),(C . (a + (Q + 1)))},{(C . (a + Q))}} is non empty set
Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a + Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . (a + Q) is set
Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a + (Q + 1) is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . (a + (Q + 1)) is set
a + 0 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . (a + 0) is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
a is set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
dom b is non empty Element of K10(NAT)
b . 2 is set
[C,(b . 2)] is set
{C,(b . 2)} is non empty set
{C} is non empty V2() V58(1) set
{{C,(b . 2)},{C}} is non empty set
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (x2 + 1) is set
b . (x2 + 1) is set
[(b . x2),(b . (x2 + 1))] is set
{(b . x2),(b . (x2 + 1))} is non empty set
{(b . x2)} is non empty V2() V58(1) set
{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (x2 + 1) is set
b . 0 is set
R is Relation-like set
C is set
a is set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
R is Relation-like set
R [*] is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() set
dom b is non empty Element of K10(NAT)
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
b . (x2 + 1) is set
[(b . x2),(b . (x2 + 1))] is set
{(b . x2),(b . (x2 + 1))} is non empty set
{(b . x2)} is non empty V2() V58(1) set
{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . 1 is set
b . (len b) is set
dom b is Element of K10(NAT)
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
b . (x2 + 1) is set
[(b . x2),(b . (x2 + 1))] is set
{(b . x2),(b . (x2 + 1))} is non empty set
{(b . x2)} is non empty V2() V58(1) set
{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set
R is Relation-like set
R [*] is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R [*] )
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
dom b is non empty Element of K10(NAT)
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (x2 + 1) is set
b . (x2 + 1) is set
[(b . x2),(b . (x2 + 1))] is set
{(b . x2),(b . (x2 + 1))} is non empty set
{(b . x2)} is non empty V2() V58(1) set
{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (x2 + 1) is set
b . 0 is set
R is Relation-like set
C is Relation-like set
a is set
b is set
x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
x2 . 1 is set
len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (len x2) is set
R is Relation-like set
C is set
id C is Relation-like C -defined C -valued Function-like one-to-one reflexive symmetric antisymmetric transitive set
R \/ (id C) is Relation-like set
a is set
b is set
x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R \/ (id C))
x2 . 1 is set
len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (len x2) is set
dom x2 is non empty Element of K10(NAT)
Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . Q is set
Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (Q + 1) is set
[(x2 . Q),(x2 . (Q + 1))] is set
{(x2 . Q),(x2 . (Q + 1))} is non empty set
{(x2 . Q)} is non empty V2() V58(1) set
{{(x2 . Q),(x2 . (Q + 1))},{(x2 . Q)}} is non empty set
x2 . (Q + 1) is set
Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . Q is set
Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (Q + 1) is set
x2 . 0 is set
R is Relation-like set
R ~ is Relation-like set
C is set
a is set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
Rev b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R ~ )
x2 . 1 is set
len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (len x2) is set
dom x2 is non empty Element of K10(NAT)
(len b) - 1 is ext-real V22() V30() set
((len b) - 1) + 1 is ext-real V22() V30() set
b . (((len b) - 1) + 1) is set
(len b) - (len b) is ext-real V22() V30() set
((len b) - (len b)) + 1 is ext-real V22() V30() set
b . (((len b) - (len b)) + 1) is set
R is Relation-like set
C is set
a is set
R ~ is Relation-like set
R \/ (R ~) is Relation-like set
(R \/ (R ~)) ~ is Relation-like set
(R ~) ~ is Relation-like set
(R ~) \/ ((R ~) ~) is Relation-like set
R is Relation-like set
C is set
a is set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
R ~ is Relation-like set
R \/ (R ~) is Relation-like set
dom b is non empty Element of K10(NAT)
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
b . (x2 + 1) is set
[(b . x2),(b . (x2 + 1))] is set
{(b . x2),(b . (x2 + 1))} is non empty set
{(b . x2)} is non empty V2() V58(1) set
{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set
R is Relation-like set
C is set
R is set
C is set
{} ~ is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
{} \/ ({} ~) is Relation-like set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
a is set
R ~ is Relation-like set
field (R ~) is set
dom (R ~) is set
rng (R ~) is set
(dom (R ~)) \/ (rng (R ~)) is set
R \/ (R ~) is Relation-like set
field (R \/ (R ~)) is set
dom (R \/ (R ~)) is set
rng (R \/ (R ~)) is set
(dom (R \/ (R ~))) \/ (rng (R \/ (R ~))) is set
(field R) \/ (field (R ~)) is set
R is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
R is Relation-like set
C is set
a is set
b is set
R ~ is Relation-like set
R \/ (R ~) is Relation-like set
R is Relation-like set
C is set
a is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
a is set
R ~ is Relation-like set
R \/ (R ~) is Relation-like set
field (R \/ (R ~)) is set
dom (R \/ (R ~)) is set
rng (R \/ (R ~)) is set
(dom (R \/ (R ~))) \/ (rng (R \/ (R ~))) is set
field (R ~) is set
dom (R ~) is set
rng (R ~) is set
(dom (R ~)) \/ (rng (R ~)) is set
(field R) \/ (field (R ~)) is set
(field R) \/ (field R) is set
R is Relation-like set
C is set
a is set
b is Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like set
len b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . 1 is set
b . (len b) is set
dom b is Element of K10(NAT)
1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (1 + 1) is set
[C,(b . (1 + 1))] is set
{C,(b . (1 + 1))} is non empty set
{C} is non empty V2() V58(1) set
{{C,(b . (1 + 1))},{C}} is non empty set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
R is Relation-like set
C is set
a is set
R is Relation-like set
C is set
a is set
b is set
b is set
R is Relation-like set
C is set
R is set
C is set
a is set
a is set
R is Relation-like set
C is set
a is set
b is set
R is Relation-like set
C is set
a is set
b is set
R is Relation-like set
C is set
a is set
b is set
x2 is set
x2 is set
R is Relation-like set
a is set
C is set
b is set
x2 is set
x2 is set
R is Relation-like set
C is set
a is set
b is set
[C,b] is set
{C,b} is non empty set
{C} is non empty V2() V58(1) set
{{C,b},{C}} is non empty set
[a,b] is set
{a,b} is non empty set
{a} is non empty V2() V58(1) set
{{a,b},{a}} is non empty set
R is Relation-like set
C is set
a is set
b is set
[b,C] is set
{b,C} is non empty set
{b} is non empty V2() V58(1) set
{{b,C},{b}} is non empty set
[b,a] is set
{b,a} is non empty set
{{b,a},{b}} is non empty set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
R is Relation-like set
C is set
a is set
b is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
R ~ is Relation-like set
field (R ~) is set
dom (R ~) is set
rng (R ~) is set
(dom (R ~)) \/ (rng (R ~)) is set
C is set
a is set
(R ~) -Seg a is set
Coim ((R ~),a) is set
{a} is non empty V2() V58(1) set
(R ~) " {a} is set
(Coim ((R ~),a)) \ {a} is Element of K10((Coim ((R ~),a)))
K10((Coim ((R ~),a))) is set
b is set
x2 is set
(R ~) -Seg b is set
Coim ((R ~),b) is set
{b} is non empty V2() V58(1) set
(R ~) " {b} is set
(Coim ((R ~),b)) \ {b} is Element of K10((Coim ((R ~),b)))
K10((Coim ((R ~),b))) is set
[x2,b] is set
{x2,b} is non empty set
{x2} is non empty V2() V58(1) set
{{x2,b},{x2}} is non empty set
[b,x2] is set
{b,x2} is non empty set
{{b,x2},{b}} is non empty set
C is set
a is set
(R ~) -Seg a is set
Coim ((R ~),a) is set
{a} is non empty V2() V58(1) set
(R ~) " {a} is set
(Coim ((R ~),a)) \ {a} is Element of K10((Coim ((R ~),a)))
K10((Coim ((R ~),a))) is set
((R ~) -Seg a) /\ C is set
b is non empty set
the Element of b is Element of b
[a, the Element of b] is set
{a, the Element of b} is non empty set
{{a, the Element of b},{a}} is non empty set
[ the Element of b,a] is set
{ the Element of b,a} is non empty set
{ the Element of b} is non empty V2() V58(1) set
{{ the Element of b,a},{ the Element of b}} is non empty set
F₁() is Relation-like set
field F₁() is set
dom F₁() is set
rng F₁() is set
(dom F₁()) \/ (rng F₁()) is set
R is set
C is non empty set
{ b₁ where b₁ is Element of C : P₁[b₁] } is set
a is Element of C
x2 is set
Q is Element of C
x2 is set
Q is set
[x2,Q] is set
{x2,Q} is non empty set
{x2} is non empty V2() V58(1) set
{{x2,Q},{x2}} is non empty set
Q is Element of C
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
[C,C] is set
{C,C} is non empty set
{C} is non empty V2() V58(1) set
{{C,C},{C}} is non empty set
NAT --> C is Relation-like Function-like V27() V35( NAT ,{C}) Element of K10(K11(NAT,{C}))
K11(NAT,{C}) is Relation-like V51() set
K10(K11(NAT,{C})) is V51() set
dom (NAT --> C) is V23() V24() V25() set
a is Relation-like NAT -defined Function-like V31( NAT ) set
b is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a . b is set
b + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
a . (b + 1) is set
[(a . b),(a . (b + 1))] is set
{(a . b),(a . (b + 1))} is non empty set
{(a . b)} is non empty V2() V58(1) set
{{(a . b),(a . (b + 1))},{(a . b)}} is non empty set
C is set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
b is set
a is non empty set
x2 is set
[b,x2] is set
{b,x2} is non empty set
{b} is non empty V2() V58(1) set
{{b,x2},{b}} is non empty set
b is set
the Element of a is Element of a
x2 is Relation-like Function-like set
dom x2 is set
rng x2 is set
x2 . 0 is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is Relation-like NAT -defined Function-like V31( NAT ) set
rng C is set
a is set
dom C is set
b is set
C . b is set
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . (x2 + 1) is set
[a,(C . (x2 + 1))] is set
{a,(C . (x2 + 1))} is non empty set
{a} is non empty V2() V58(1) set
{{a,(C . (x2 + 1))},{a}} is non empty set
dom C is set
C . 0 is set
a is set
b is set
C . b is set
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
C . (x2 + 1) is set
[a,(C . (x2 + 1))] is set
{a,(C . (x2 + 1))} is non empty set
{a} is non empty V2() V58(1) set
{{a,(C . (x2 + 1))},{a}} is non empty set
R is Relation-like set
C is set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is Relation-like NAT -defined Function-like V31( NAT ) set
C . 0 is set
C . (0 + 1) is set
[(C . 0),(C . (0 + 1))] is set
{(C . 0),(C . (0 + 1))} is non empty set
{(C . 0)} is non empty V2() V58(1) set
{{(C . 0),(C . (0 + 1))},{(C . 0)}} is non empty set
R is Relation-like () set
C is Relation-like set
a is set
field C is set
dom C is set
rng C is set
(dom C) \/ (rng C) is set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
b is set
x2 is set
[b,x2] is set
{b,x2} is non empty set
{b} is non empty V2() V58(1) set
{{b,x2},{b}} is non empty set
R is Relation-like set
C is set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
a is non empty set
{ b₁ where b₁ is Element of a : (R,C,b₁) } is set
x2 is set
Q is Element of a
x2 is set
[x2,x2] is set
{x2,x2} is non empty set
{x2} is non empty V2() V58(1) set
{{x2,x2},{x2}} is non empty set
Q is set
[x2,Q] is set
{x2,Q} is non empty set
{{x2,Q},{x2}} is non empty set
X is Element of a
Q is Element of a
a is Relation-like set
b is Relation-like set
x2 is set
Q is set
[x2,Q] is set
{x2,Q} is non empty set
{x2} is non empty V2() V58(1) set
{{x2,Q},{x2}} is non empty set
X is set
[x2,X] is set
{x2,X} is non empty set
{{x2,X},{x2}} is non empty set
P is set
a is Relation-like set
b is Relation-like set
x2 is set
Q is set
X is set
P is set
R is Relation-like set
C is Relation-like set
a is set
b is set
[a,b] is set
{a,b} is non empty set
{a} is non empty V2() V58(1) set
{{a,b},{a}} is non empty set
x2 is set
[a,x2] is set
{a,x2} is non empty set
{{a,x2},{a}} is non empty set
R is Relation-like set
C is set
a is set
b is set
[C,b] is set
{C,b} is non empty set
{C} is non empty V2() V58(1) set
{{C,b},{C}} is non empty set
x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
x2 . 1 is set
len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (len x2) is set
dom x2 is non empty Element of K10(NAT)
Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . Q is set
Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (Q + 1) is set
X is set
[(x2 . Q),X] is set
{(x2 . Q),X} is non empty set
{(x2 . Q)} is non empty V2() V58(1) set
{{(x2 . Q),X},{(x2 . Q)}} is non empty set
X is set
[(x2 . Q),X] is set
{(x2 . Q),X} is non empty set
{(x2 . Q)} is non empty V2() V58(1) set
{{(x2 . Q),X},{(x2 . Q)}} is non empty set
x2 . (Q + 1) is set
[(x2 . Q),(x2 . (Q + 1))] is set
{(x2 . Q),(x2 . (Q + 1))} is non empty set
{{(x2 . Q),(x2 . (Q + 1))},{(x2 . Q)}} is non empty set
P is set
[(x2 . (Q + 1)),P] is set
{(x2 . (Q + 1)),P} is non empty set
{(x2 . (Q + 1))} is non empty V2() V58(1) set
{{(x2 . (Q + 1)),P},{(x2 . (Q + 1))}} is non empty set
[X,P] is set
{X,P} is non empty set
{X} is non empty V2() V58(1) set
{{X,P},{X}} is non empty set
P is set
[(x2 . (Q + 1)),P] is set
{(x2 . (Q + 1)),P} is non empty set
{{(x2 . (Q + 1)),P},{(x2 . (Q + 1))}} is non empty set
P is set
[(x2 . (Q + 1)),P] is set
{(x2 . (Q + 1)),P} is non empty set
{{(x2 . (Q + 1)),P},{(x2 . (Q + 1))}} is non empty set
Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . Q is set
X is set
[(x2 . Q),X] is set
{(x2 . Q),X} is non empty set
{(x2 . Q)} is non empty V2() V58(1) set
{{(x2 . Q),X},{(x2 . Q)}} is non empty set
Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (Q + 1) is set
x2 . 0 is set
Q is set
[a,Q] is set
{a,Q} is non empty set
{a} is non empty V2() V58(1) set
{{a,Q},{a}} is non empty set
R is Relation-like set
C is set
a is set
b is set
C is set
a is set
b is set
R is Relation-like set
C is set
a is set
b is set
[C,b] is set
{C,b} is non empty set
{C} is non empty V2() V58(1) set
{{C,b},{C}} is non empty set
C is set
a is set
b is set
x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
x2 . 1 is set
len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (len x2) is set
Q is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
Q . 1 is set
len Q is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . (len Q) is set
dom x2 is non empty Element of K10(NAT)
dom Q is non empty Element of K10(NAT)
X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . X is set
X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (X + 1) is set
P is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . P is set
P + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . (P + 1) is set
P is set
[(Q . P),(Q . (P + 1))] is set
{(Q . P),(Q . (P + 1))} is non empty set
{(Q . P)} is non empty V2() V58(1) set
{{(Q . P),(Q . (P + 1))},{(Q . P)}} is non empty set
Q . 0 is set
x2 . 0 is set
X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . X is set
R is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
b is set
[C,b] is set
{C,b} is non empty set
{{C,b},{C}} is non empty set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
b is set
[C,b] is set
{C,b} is non empty set
{{C,b},{C}} is non empty set
R is Relation-like set
C is set
a is set
R is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
b is set
[C,b] is set
{C,b} is non empty set
{{C,b},{C}} is non empty set
C is set
a is set
R ~ is Relation-like set
R \/ (R ~) is Relation-like set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R \/ (R ~))
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
dom b is non empty Element of K10(NAT)
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q is set
b . (x2 + 1) is set
[(b . x2),(b . (x2 + 1))] is set
{(b . x2),(b . (x2 + 1))} is non empty set
{(b . x2)} is non empty V2() V58(1) set
{{(b . x2),(b . (x2 + 1))},{(b . x2)}} is non empty set
[(b . (x2 + 1)),(b . x2)] is set
{(b . (x2 + 1)),(b . x2)} is non empty set
{(b . (x2 + 1))} is non empty V2() V58(1) set
{{(b . (x2 + 1)),(b . x2)},{(b . (x2 + 1))}} is non empty set
b . (x2 + 1) is set
x2 is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . x2 is set
x2 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (x2 + 1) is set
b . 0 is set
R is Relation-like set
C is set
a is set
b is set
[C,b] is set
{C,b} is non empty set
{C} is non empty V2() V58(1) set
{{C,b},{C}} is non empty set
R is Relation-like set
C is set
a is set
b is set
R is Relation-like set
C is set
a is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
a is set
R ~ is Relation-like set
R \/ (R ~) is Relation-like set
field (R \/ (R ~)) is set
dom (R \/ (R ~)) is set
rng (R \/ (R ~)) is set
(dom (R \/ (R ~))) \/ (rng (R \/ (R ~))) is set
field (R ~) is set
dom (R ~) is set
rng (R ~) is set
(dom (R ~)) \/ (rng (R ~)) is set
(field R) \/ (field (R ~)) is set
(field R) \/ (field R) is set
b is set
x2 is set
R is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
b is set
[C,b] is set
{C,b} is non empty set
{{C,b},{C}} is non empty set
R is Relation-like () set
C is set
a is set
b is set
R is Relation-like () () () () () () set
C is set
(R,C) is set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
a is set
b is set
R is Relation-like () () () () () () set
C is set
a is set
(R,C) is set
(R,a) is set
R is Relation-like set
C is set
a is set
b is set
x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
x2 . 1 is set
len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (len x2) is set
Q is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R)
Q . 1 is set
len Q is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . (len Q) is set
1 + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
dom Q is non empty Element of K10(NAT)
Q . 2 is set
dom x2 is non empty Element of K10(NAT)
x2 . 2 is set
[C,(x2 . 2)] is set
{C,(x2 . 2)} is non empty set
{C} is non empty V2() V58(1) set
{{C,(x2 . 2)},{C}} is non empty set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
[C,(Q . 2)] is set
{C,(Q . 2)} is non empty set
{{C,(Q . 2)},{C}} is non empty set
X is set
P is set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is set
a is set
b is set
R is Relation-like set
R is Relation-like set
[0,1] is set
{0,1} is non empty set
{0} is non empty V2() functional V58(1) set
{{0,1},{0}} is non empty set
{[0,1]} is non empty V2() Relation-like Function-like constant V58(1) set
R is non empty Relation-like set
field R is set
dom R is non empty set
rng R is non empty set
(dom R) \/ (rng R) is non empty set
C is set
a is set
b is set
C is set
a is non empty set
the Element of a is Element of a
x2 is set
[1,x2] is set
{1,x2} is non empty set
{{1,x2},{1}} is non empty set
x2 is set
[0,x2] is set
{0,x2} is non empty set
{{0,x2},{0}} is non empty set
C is set
[C,C] is set
{C,C} is non empty set
{C} is non empty V2() V58(1) set
{{C,C},{C}} is non empty set
R is Relation-like () () () () () set
C is Relation-like () () () () () set
R \/ C is Relation-like set
a is set
b is set
x2 is set
Q is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R \/ C)
Q . 1 is set
len Q is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . (len Q) is set
dom Q is non empty Element of K10(NAT)
X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . X is set
X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . (X + 1) is set
P is set
P is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (R \/ C)
P . 1 is set
len P is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
P . (len P) is set
dom P is non empty Element of K10(NAT)
Q . (X + 1) is set
[(Q . X),(Q . (X + 1))] is set
{(Q . X),(Q . (X + 1))} is non empty set
{(Q . X)} is non empty V2() V58(1) set
{{(Q . X),(Q . (X + 1))},{(Q . X)}} is non empty set
a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
P . a is set
a + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
P . (a + 1) is set
b is set
b is set
P . (a + 1) is set
c is set
c₁₃ is set
c is set
c₁₃ is set
c is set
c₁₃ is set
c is set
c₁₃ is set
[(P . a),(P . (a + 1))] is set
{(P . a),(P . (a + 1))} is non empty set
{(P . a)} is non empty V2() V58(1) set
{{(P . a),(P . (a + 1))},{(P . a)}} is non empty set
c is set
c₁₃ is set
c₁₄ is set
c₁₅ is set
a is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b is set
P . a is set
a + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
P . (a + 1) is set
P . 0 is set
a is set
X is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . X is set
X + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
Q . (X + 1) is set
Q . 0 is set
R is Relation-like set
R [*] is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
b is set
[C,b] is set
{C,b} is non empty set
{{C,b},{C}} is non empty set
x2 is set
C is set
a is set
b is set
[b,a] is set
{b,a} is non empty set
{b} is non empty V2() V58(1) set
{{b,a},{b}} is non empty set
[b,C] is set
{b,C} is non empty set
{{b,C},{b}} is non empty set
x2 is set
R is Relation-like set
R [*] is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
b is set
[C,b] is set
{C,b} is non empty set
{{C,b},{C}} is non empty set
x2 is set
[a,x2] is set
{a,x2} is non empty set
{a} is non empty V2() V58(1) set
{{a,x2},{a}} is non empty set
[b,x2] is set
{b,x2} is non empty set
{b} is non empty V2() V58(1) set
{{b,x2},{b}} is non empty set
C is set
a is set
b is set
[b,a] is set
{b,a} is non empty set
{b} is non empty V2() V58(1) set
{{b,a},{b}} is non empty set
[b,C] is set
{b,C} is non empty set
{{b,C},{b}} is non empty set
x2 is set
a is Relation-like set
b is Relation-like set
x2 is set
Q is set
X is set
P is set
R is Relation-like set
C is set
a is set
R is Relation-like set
C is set
a is set
[C,a] is set
{C,a} is non empty set
{C} is non empty V2() V58(1) set
{{C,a},{C}} is non empty set
b is set
[C,b] is set
{C,b} is non empty set
{{C,b},{C}} is non empty set
C is Relation-like set
R is Relation-like set
R \/ C is Relation-like set
a is set
b is set
R ~ is Relation-like set
(R \/ C) ~ is Relation-like set
x2 is set
Q is set
[x2,Q] is set
{x2,Q} is non empty set
{x2} is non empty V2() V58(1) set
{{x2,Q},{x2}} is non empty set
[Q,x2] is set
{Q,x2} is non empty set
{Q} is non empty V2() V58(1) set
{{Q,x2},{Q}} is non empty set
R \/ (R ~) is Relation-like set
(R \/ C) \/ ((R \/ C) ~) is Relation-like set
x2 is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like ((R \/ C) \/ ((R \/ C) ~))
x2 . 1 is set
len x2 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (len x2) is set
dom x2 is non empty Element of K10(NAT)
Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . Q is set
Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (Q + 1) is set
x2 . (Q + 1) is set
[(x2 . Q),(x2 . (Q + 1))] is set
{(x2 . Q),(x2 . (Q + 1))} is non empty set
{(x2 . Q)} is non empty V2() V58(1) set
{{(x2 . Q),(x2 . (Q + 1))},{(x2 . Q)}} is non empty set
[(x2 . (Q + 1)),(x2 . Q)] is set
{(x2 . (Q + 1)),(x2 . Q)} is non empty set
{(x2 . (Q + 1))} is non empty V2() V58(1) set
{{(x2 . (Q + 1)),(x2 . Q)},{(x2 . (Q + 1))}} is non empty set
Q is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . Q is set
Q + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
x2 . (Q + 1) is set
x2 . 0 is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() irreflexive V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () () () () () set
field C is set
dom C is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() irreflexive V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () () () () () set
rng C is empty V2() V4() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative V22() V23() V24() V25() V27() V28() V29() V30() irreflexive V51() V56() V58( {} ) FinSequence-like FinSubsequence-like FinSequence-membered () () () () () () () () () () set
(dom C) \/ (rng C) is Relation-like set
a is set
b is set
C is non empty Relation-like set
the Element of C is Element of C
b is set
x2 is set
[b,x2] is set
{b,x2} is non empty set
{b} is non empty V2() V58(1) set
{{b,x2},{b}} is non empty set
Q is set
X is set
Q is set
X is set
P is set
Q is set
K11((field R),(field R)) is Relation-like set
K10(K11((field R),(field R))) is set
Q is Relation-like V31( field R) reflexive symmetric transitive Element of K10(K11((field R),(field R)))
Class Q is a_partition of field R
X is set
P is set
P is set
Class (Q,b) is Element of K10((field R))
K10((field R)) is set
Q .: {b} is set
X is set
P is Relation-like set
P is set
a is set
[P,a] is set
{P,a} is non empty set
{P} is non empty V2() V58(1) set
{{P,a},{P}} is non empty set
b is set
[P,b] is set
{P,b} is non empty set
{{P,b},{P}} is non empty set
Class (Q,P) is Element of K10((field R))
Q .: {P} is set
X /\ (Class (Q,P)) is Element of K10((field R))
c is set
{c} is non empty V2() V58(1) set
[b,P] is set
{b,P} is non empty set
{b} is non empty V2() V58(1) set
{{b,P},{b}} is non empty set
[a,P] is set
{a,P} is non empty set
{a} is non empty V2() V58(1) set
{{a,P},{a}} is non empty set
P is set
a is set
b is non empty Relation-like NAT -defined Function-like V51() FinSequence-like FinSubsequence-like (P)
b . 1 is set
len b is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (len b) is set
dom b is non empty Element of K10(NAT)
c is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . c is set
c + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (c + 1) is set
b . (c + 1) is set
[(b . c),(b . (c + 1))] is set
{(b . c),(b . (c + 1))} is non empty set
{(b . c)} is non empty V2() V58(1) set
{{(b . c),(b . (c + 1))},{(b . c)}} is non empty set
c is ext-real non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . c is set
c + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
b . (c + 1) is set
b . 0 is set
P is Relation-like NAT -defined Function-like V31( NAT ) set
P . 0 is set
P . (0 + 1) is set
[(P . 0),(P . (0 + 1))] is set
{(P . 0),(P . (0 + 1))} is non empty set
{(P . 0)} is non empty V2() V58(1) set
{{(P . 0),(P . (0 + 1))},{(P . 0)}} is non empty set
P . 0 is set
P . (0 + 1) is set
[(P . 0),(P . (0 + 1))] is set
{(P . 0),(P . (0 + 1))} is non empty set
{(P . 0)} is non empty V2() V58(1) set
{{(P . 0),(P . (0 + 1))},{(P . 0)}} is non empty set
a is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
P . a is set
a + 1 is non empty ext-real positive non negative V22() V23() V24() V25() V29() V30() V51() V56() Element of NAT
P . (a + 1) is set
[(P . a),(P . (a + 1))] is set
{(P . a),(P . (a + 1))} is non empty set
{(P . a)} is non empty V2() V58(1) set
{{(P . a),(P . (a + 1))},{(P . a)}} is non empty set
Class (Q,(P . a)) is Element of K10((field R))
Q .: {(P . a)} is set
X /\ (Class (Q,(P . a))) is Element of K10((field R))
b is set
{b} is non empty V2() V58(1) set
[(P . (a + 1)),(P . a)] is set
{(P . (a + 1)),(P . a)} is non empty set
{(P . (a + 1))} is non empty V2() V58(1) set
{{(P . (a + 1)),(P . a)},{(P . (a + 1))}} is non empty set
P . 0 is set
P . (0 + 1) is set
[(P . 0),(P . (0 + 1))] is set
{(P . 0),(P . (0 + 1))} is non empty set
{(P . 0)} is non empty V2() V58(1) set
{{(P . 0),(P . (0 + 1))},{(P . 0)}} is non empty set
P is Relation-like irreflexive () () () () () () () () () set
field P is set
dom P is set
rng P is set
(dom P) \/ (rng P) is set
a is set
b is set
[a,b] is set
{a,b} is non empty set
{a} is non empty V2() V58(1) set
{{a,b},{a}} is non empty set
c is set
[c,a] is set
{c,a} is non empty set
{c} is non empty V2() V58(1) set
{{c,a},{c}} is non empty set
a is set
b is set
Class (Q,b) is Element of K10((field R))
{b} is non empty V2() V58(1) set
Q .: {b} is set
X /\ (Class (Q,b)) is Element of K10((field R))
c is set
{c} is non empty V2() V58(1) set
[a,b] is set
{a,b} is non empty set
{a} is non empty V2() V58(1) set
{{a,b},{a}} is non empty set
[c,b] is set
{c,b} is non empty set
{{c,b},{c}} is non empty set
[b,c] is set
{b,c} is non empty set
{{b,c},{b}} is non empty set
[a,c] is set
{a,c} is non empty set
{{a,c},{a}} is non empty set
c is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
C is Relation-like irreflexive () () () () () () () () () set
field C is set
dom C is set
rng C is set
(dom C) \/ (rng C) is set
R is Relation-like set
C is Relation-like irreflexive () () () () () () () () () (R)
a is set
b is set
R is Relation-like set
C is Relation-like irreflexive () () () () () () () () () set
a is set
b is set
R is Relation-like set
C is Relation-like irreflexive () () () () () () () () () (R)
a is set
b is set
(C,a) is set
(C,b) is set