:: SCHEME1 semantic presentation

REAL is non empty set
NAT is non empty V18() V19() V20() Element of bool REAL
bool REAL is set
COMPLEX is non empty set
RAT is non empty set
INT is non empty set
0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
the empty ext-real non positive non negative V18() V19() V20() V22() V23() V24() V25() V32() set is empty ext-real non positive non negative V18() V19() V20() V22() V23() V24() V25() V32() set
1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
{} is set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is set
NAT is non empty V18() V19() V20() set
2 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
f div 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
2 * (f div 2) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(2 * (f div 2)) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
f mod 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(2 * (f div 2)) + (f mod 2) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
f div 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 * (f div 3) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * (f div 3)) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * (f div 3)) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
f mod 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * (f div 3)) + (f mod 3) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
f div 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * (f div 4) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * (f div 4)) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * (f div 4)) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * (f div 4)) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
f mod 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
(4 * (f div 4)) + (f mod 4) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
f div 5 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * (f div 5) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * (f div 5)) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * (f div 5)) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * (f div 5)) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * (f div 5)) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
f mod 5 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
3 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
0 + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
2 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() Element of NAT
(5 * (f div 5)) + (f mod 5) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
f is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . f is ext-real V25() V32() Element of REAL
f is ext-real V18() V19() V20() V24() V25() V32() set
F₁() . f is ext-real V25() V32() Element of REAL
v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
v + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c₄ is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . c₄ is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . z is ext-real V25() V32() Element of REAL
v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c₄ is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . z is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() set
F₁() . z is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . x is ext-real V25() V32() Element of REAL
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . d is ext-real V25() V32() Element of REAL
[:NAT,NAT:] is set
bool [:NAT,NAT:] is set
v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
v is Relation-like NAT -defined NAT -valued Function-like V29( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
v . 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
dom v is Element of bool NAT
bool NAT is set
rng v is V46() V47() V48() V51() Element of bool NAT
c₄ is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,REAL:]
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c₄ . (z + 1) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c₄ . z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z is Relation-like NAT -defined NAT -valued Function-like V29( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . z is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() set
F₁() . z is ext-real V25() V32() Element of REAL
z . 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V18() V19() V20() V24() V25() V32() set
F₁() . y is ext-real V25() V32() Element of REAL
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V18() V19() V20() V24() V25() V32() set
F₁() . y is ext-real V25() V32() Element of REAL
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . x is ext-real V25() V32() Element of REAL
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c₁₀ is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . c₁₀ is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . (x + 1) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . (z . (x + 1)) is ext-real V25() V32() Element of REAL
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() * z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of F₁()
z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of F₁()
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . y is ext-real V25() V32() Element of REAL
y + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . (y + 1) is ext-real V25() V32() Element of REAL
z . y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . (y + 1) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . d is ext-real V25() V32() Element of REAL
c₁₀ is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . c₁₀ is ext-real V25() V32() Element of REAL
F₁() . (z . (y + 1)) is ext-real V25() V32() Element of REAL
z . 0 is ext-real V25() V32() Element of REAL
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F₁() . y is ext-real V25() V32() Element of REAL
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . x is ext-real V25() V32() Element of REAL
bool NAT is set
f is Element of bool NAT
v is Element of bool NAT
v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
v / 2 is ext-real V25() V32() set
F₁((v / 2)) is ext-real V25() V32() Element of REAL
v - 1 is ext-real V25() V32() set
(v - 1) / 2 is ext-real V25() V32() set
F₂(((v - 1) / 2)) is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
2 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(2 * z) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
2 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(2 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z is ext-real V25() V32() Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
c₄ is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
2 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c₄ . (2 * z) is ext-real V25() V32() Element of REAL
F₁(z) is ext-real V25() V32() Element of REAL
(2 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c₄ . ((2 * z) + 1) is ext-real V25() V32() Element of REAL
F₂(z) is ext-real V25() V32() Element of REAL
(2 * z) / 2 is ext-real V25() V32() set
F₁(((2 * z) / 2)) is ext-real V25() V32() Element of REAL
((2 * z) + 1) - 1 is ext-real V25() V32() set
(((2 * z) + 1) - 1) / 2 is ext-real V25() V32() set
F₂(((((2 * z) + 1) - 1) / 2)) is ext-real V25() V32() Element of REAL
bool NAT is set
f is Element of bool NAT
v is Element of bool NAT
v is Element of bool NAT
c₄ is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c₄ / 3 is ext-real V25() V32() set
F₁((c₄ / 3)) is ext-real V25() V32() Element of REAL
c₄ - 1 is ext-real V25() V32() set
(c₄ - 1) / 3 is ext-real V25() V32() set
F₂(((c₄ - 1) / 3)) is ext-real V25() V32() Element of REAL
c₄ - 2 is ext-real V25() V32() set
(c₄ - 2) / 3 is ext-real V25() V32() set
F₃(((c₄ - 2) / 3)) is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * z) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * z) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * y) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * y) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * y) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * y) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * y) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(3 * y) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y is ext-real V25() V32() Element of REAL
c₄ is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
3 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . (3 * z) is ext-real V25() V32() Element of REAL
F₁(z) is ext-real V25() V32() Element of REAL
(3 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . ((3 * z) + 1) is ext-real V25() V32() Element of REAL
F₂(z) is ext-real V25() V32() Element of REAL
(3 * z) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . ((3 * z) + 2) is ext-real V25() V32() Element of REAL
F₃(z) is ext-real V25() V32() Element of REAL
(3 * z) / 3 is ext-real V25() V32() set
F₁(((3 * z) / 3)) is ext-real V25() V32() Element of REAL
((3 * z) + 1) - 1 is ext-real V25() V32() set
(((3 * z) + 1) - 1) / 3 is ext-real V25() V32() set
F₂(((((3 * z) + 1) - 1) / 3)) is ext-real V25() V32() Element of REAL
((3 * z) + 2) - 2 is ext-real V25() V32() set
(((3 * z) + 2) - 2) / 3 is ext-real V25() V32() set
F₃(((((3 * z) + 2) - 2) / 3)) is ext-real V25() V32() Element of REAL
bool NAT is set
f is Element of bool NAT
v is Element of bool NAT
v is Element of bool NAT
c₄ is Element of bool NAT
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z / 4 is ext-real V25() V32() set
F₁((z / 4)) is ext-real V25() V32() Element of REAL
z - 1 is ext-real V25() V32() set
(z - 1) / 4 is ext-real V25() V32() set
F₂(((z - 1) / 4)) is ext-real V25() V32() Element of REAL
z - 2 is ext-real V25() V32() set
(z - 2) / 4 is ext-real V25() V32() set
F₃(((z - 2) / 4)) is ext-real V25() V32() Element of REAL
z - 3 is ext-real V25() V32() set
(z - 3) / 4 is ext-real V25() V32() set
F₄(((z - 3) / 4)) is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * z) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * z) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * z) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(4 * x) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V25() V32() Element of REAL
z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
4 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . (4 * y) is ext-real V25() V32() Element of REAL
F₁(y) is ext-real V25() V32() Element of REAL
(4 * y) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . ((4 * y) + 1) is ext-real V25() V32() Element of REAL
F₂(y) is ext-real V25() V32() Element of REAL
(4 * y) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . ((4 * y) + 2) is ext-real V25() V32() Element of REAL
F₃(y) is ext-real V25() V32() Element of REAL
(4 * y) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . ((4 * y) + 3) is ext-real V25() V32() Element of REAL
F₄(y) is ext-real V25() V32() Element of REAL
(4 * y) / 4 is ext-real V25() V32() set
F₁(((4 * y) / 4)) is ext-real V25() V32() Element of REAL
((4 * y) + 1) - 1 is ext-real V25() V32() set
(((4 * y) + 1) - 1) / 4 is ext-real V25() V32() set
F₂(((((4 * y) + 1) - 1) / 4)) is ext-real V25() V32() Element of REAL
((4 * y) + 2) - 2 is ext-real V25() V32() set
(((4 * y) + 2) - 2) / 4 is ext-real V25() V32() set
F₃(((((4 * y) + 2) - 2) / 4)) is ext-real V25() V32() Element of REAL
((4 * y) + 3) - 3 is ext-real V25() V32() set
(((4 * y) + 3) - 3) / 4 is ext-real V25() V32() set
F₄(((((4 * y) + 3) - 3) / 4)) is ext-real V25() V32() Element of REAL
bool NAT is set
f is Element of bool NAT
v is Element of bool NAT
v is Element of bool NAT
c₄ is Element of bool NAT
z is Element of bool NAT
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z / 5 is ext-real V25() V32() set
F₁((z / 5)) is ext-real V25() V32() Element of REAL
z - 1 is ext-real V25() V32() set
(z - 1) / 5 is ext-real V25() V32() set
F₂(((z - 1) / 5)) is ext-real V25() V32() Element of REAL
z - 2 is ext-real V25() V32() set
(z - 2) / 5 is ext-real V25() V32() set
F₃(((z - 2) / 5)) is ext-real V25() V32() Element of REAL
z - 3 is ext-real V25() V32() set
(z - 3) / 5 is ext-real V25() V32() set
F₄(((z - 3) / 5)) is ext-real V25() V32() Element of REAL
z - 4 is ext-real V25() V32() set
(z - 4) / 5 is ext-real V25() V32() set
F₅(((z - 4) / 5)) is ext-real V25() V32() Element of REAL
y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * y is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * y) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * y) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * y) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * y) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * y) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * x) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * x) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * x) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
(5 * d) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
d is ext-real V25() V32() Element of REAL
z is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
y is Relation-like NAT -defined REAL -valued Function-like V29( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
5 * x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y . (5 * x) is ext-real V25() V32() Element of REAL
F₁(x) is ext-real V25() V32() Element of REAL
(5 * x) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y . ((5 * x) + 1) is ext-real V25() V32() Element of REAL
F₂(x) is ext-real V25() V32() Element of REAL
(5 * x) + 2 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y . ((5 * x) + 2) is ext-real V25() V32() Element of REAL
F₃(x) is ext-real V25() V32() Element of REAL
(5 * x) + 3 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y . ((5 * x) + 3) is ext-real V25() V32() Element of REAL
F₄(x) is ext-real V25() V32() Element of REAL
(5 * x) + 4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
y . ((5 * x) + 4) is ext-real V25() V32() Element of REAL
F₅(x) is ext-real V25() V32() Element of REAL
(5 * x) / 5 is ext-real V25() V32() set
F₁(((5 * x) / 5)) is ext-real V25() V32() Element of REAL
((5 * x) + 1) - 1 is ext-real V25() V32() set
(((5 * x) + 1) - 1) / 5 is ext-real V25() V32() set
F₂(((((5 * x) + 1) - 1) / 5)) is ext-real V25() V32() Element of REAL
((5 * x) + 2) - 2 is ext-real V25() V32() set
(((5 * x) + 2) - 2) / 5 is ext-real V25() V32() set
F₃(((((5 * x) + 2) - 2) / 5)) is ext-real V25() V32() Element of REAL
((5 * x) + 3) - 3 is ext-real V25() V32() set
(((5 * x) + 3) - 3) / 5 is ext-real V25() V32() set
F₄(((((5 * x) + 3) - 3) / 5)) is ext-real V25() V32() Element of REAL
((5 * x) + 4) - 4 is ext-real V25() V32() set
(((5 * x) + 4) - 4) / 5 is ext-real V25() V32() set
F₅(((((5 * x) + 4) - 4) / 5)) is ext-real V25() V32() Element of REAL
F₂() is non empty set
F₁() is non empty set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is set
v is set
F₃(v) is Element of F₂()
F₄(v) is Element of F₂()
v is Element of F₁()
v is Element of F₁()
z is set
v is Relation-like Function-like set
dom v is set
v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
v is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom v is Element of bool F₁()
bool F₁() is set
c₄ is Element of F₁()
z is Element of F₁()
c₄ is Element of F₁()
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₂() is non empty set
F₁() is non empty set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is set
v is set
F₃(v) is Element of F₂()
F₄(v) is Element of F₂()
v is Element of F₁()
F₃(v) is Element of F₂()
F₄(v) is Element of F₂()
z is set
v is Element of F₁()
F₄(v) is Element of F₂()
F₃(v) is Element of F₂()
z is set
v is Element of F₁()
z is set
v is Relation-like Function-like set
dom v is set
v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
v is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom v is Element of bool F₁()
bool F₁() is set
c₄ is Element of F₁()
z is Element of F₁()
c₄ is Element of F₁()
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₂() is non empty set
F₁() is non empty set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is Element of F₁()
f is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom f is Element of bool F₁()
bool F₁() is set
v is set
v is Element of F₁()
v is Element of F₁()
f . v is set
F₃(v) is Element of F₂()
F₄(v) is Element of F₂()
F₂() is non empty set
F₁() is non empty set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is set
v is set
F₃(v) is Element of F₂()
F₄(v) is Element of F₂()
F₅(v) is Element of F₂()
v is Element of F₁()
v is Element of F₁()
v is Element of F₁()
z is set
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₅(c₄) is Element of F₂()
v is set
v is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom v is Element of bool F₁()
bool F₁() is set
c₄ is Element of F₁()
z is Element of F₁()
c₄ is Element of F₁()
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₅(c₄) is Element of F₂()
F₂() is non empty set
F₁() is non empty set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is set
v is set
F₃(v) is Element of F₂()
F₄(v) is Element of F₂()
F₅(v) is Element of F₂()
v is Element of F₁()
F₃(v) is Element of F₂()
F₄(v) is Element of F₂()
F₅(v) is Element of F₂()
z is set
F₅(v) is Element of F₂()
z is set
z is set
v is Element of F₁()
F₃(v) is Element of F₂()
F₄(v) is Element of F₂()
F₅(v) is Element of F₂()
z is set
F₄(v) is Element of F₂()
F₅(v) is Element of F₂()
z is set
z is set
v is Element of F₁()
F₃(v) is Element of F₂()
F₅(v) is Element of F₂()
F₄(v) is Element of F₂()
z is set
F₄(v) is Element of F₂()
F₅(v) is Element of F₂()
z is set
z is set
v is Element of F₁()
z is set
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₅(c₄) is Element of F₂()
v is set
v is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom v is Element of bool F₁()
bool F₁() is set
c₄ is Element of F₁()
z is Element of F₁()
c₄ is Element of F₁()
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₅(c₄) is Element of F₂()
F₂() is non empty set
F₁() is non empty set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is set
v is set
F₃(v) is Element of F₂()
F₄(v) is Element of F₂()
F₅(v) is Element of F₂()
F₆(v) is Element of F₂()
v is Element of F₁()
v is Element of F₁()
v is Element of F₁()
v is Element of F₁()
z is set
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₅(c₄) is Element of F₂()
F₆(c₄) is Element of F₂()
v is set
v is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom v is Element of bool F₁()
bool F₁() is set
c₄ is Element of F₁()
z is Element of F₁()
c₄ is Element of F₁()
v . c₄ is set
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₅(c₄) is Element of F₂()
F₆(c₄) is Element of F₂()
F₁() is set
F₂() is set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is set
v is set
F₃(v) is set
F₄(v) is set
c₄ is set
v is Relation-like Function-like set
dom v is set
v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
F₃(c₄) is set
F₄(c₄) is set
v is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom v is Element of bool F₁()
bool F₁() is set
c₄ is set
z is set
c₄ is set
v . c₄ is set
F₃(c₄) is set
F₄(c₄) is set
F₁() is set
F₂() is set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is set
v is set
F₃(v) is set
F₄(v) is set
F₅(v) is set
c₄ is set
v is Relation-like Function-like set
dom v is set
v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
F₃(c₄) is set
F₄(c₄) is set
F₅(c₄) is set
v is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom v is Element of bool F₁()
bool F₁() is set
c₄ is set
z is set
c₄ is set
v . c₄ is set
F₃(c₄) is set
F₄(c₄) is set
F₅(c₄) is set
F₁() is set
F₂() is set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is set
v is set
F₃(v) is set
F₄(v) is set
F₅(v) is set
F₆(v) is set
c₄ is set
v is Relation-like Function-like set
dom v is set
v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
F₃(c₄) is set
F₄(c₄) is set
F₅(c₄) is set
F₆(c₄) is set
v is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom v is Element of bool F₁()
bool F₁() is set
c₄ is set
z is set
c₄ is set
v . c₄ is set
F₃(c₄) is set
F₄(c₄) is set
F₅(c₄) is set
F₆(c₄) is set
F₃() is non empty set
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is set
[:[:F₁(),F₂():],F₃():] is set
bool [:[:F₁(),F₂():],F₃():] is set
f is set
v is set
v is set
c₄ is set
[v,c₄] is set
{v,c₄} is set
{v} is set
{{v,c₄},{v}} is set
z is Element of F₁()
z is Element of F₂()
F₄(z,z) is Element of F₃()
x is Element of F₁()
d is Element of F₂()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F₃()
F₄(x,d) is Element of F₃()
F₅(x,d) is Element of F₃()
z is Element of F₁()
z is Element of F₂()
F₅(z,z) is Element of F₃()
x is Element of F₁()
d is Element of F₂()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F₃()
F₄(x,d) is Element of F₃()
F₅(x,d) is Element of F₃()
z is Element of F₁()
z is Element of F₂()
y is Element of F₃()
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
z is set
z is set
[z,z] is set
{z,z} is set
{z} is set
{{z,z},{z}} is set
x is Element of F₁()
y is Element of F₂()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F₄(x,y) is Element of F₃()
x is Element of F₁()
y is Element of F₂()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F₅(x,y) is Element of F₃()
x is Element of F₁()
y is Element of F₂()
v is set
v is Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like Element of bool [:[:F₁(),F₂():],F₃():]
dom v is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
bool [:F₁(),F₂():] is set
c₄ is Element of F₁()
z is Element of F₂()
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
z is Element of F₁()
y is Element of F₂()
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
c₄ is Element of F₁()
z is Element of F₂()
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
v . [c₄,z] is set
F₄(c₄,z) is Element of F₃()
F₅(c₄,z) is Element of F₃()
F₃() is non empty set
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is set
[:[:F₁(),F₂():],F₃():] is set
bool [:[:F₁(),F₂():],F₃():] is set
f is set
v is set
v is set
c₄ is set
[v,c₄] is set
{v,c₄} is set
{v} is set
{{v,c₄},{v}} is set
z is Element of F₁()
z is Element of F₂()
F₄(z,z) is Element of F₃()
x is Element of F₁()
d is Element of F₂()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F₃()
F₄(x,d) is Element of F₃()
F₅(x,d) is Element of F₃()
F₆(x,d) is Element of F₃()
z is Element of F₁()
z is Element of F₂()
F₅(z,z) is Element of F₃()
x is Element of F₁()
d is Element of F₂()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F₃()
F₄(x,d) is Element of F₃()
F₅(x,d) is Element of F₃()
F₆(x,d) is Element of F₃()
z is Element of F₁()
z is Element of F₂()
F₆(z,z) is Element of F₃()
x is Element of F₁()
d is Element of F₂()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F₃()
F₄(x,d) is Element of F₃()
F₅(x,d) is Element of F₃()
F₆(x,d) is Element of F₃()
z is Element of F₁()
z is Element of F₂()
y is Element of F₃()
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
z is set
z is set
[z,z] is set
{z,z} is set
{z} is set
{{z,z},{z}} is set
x is Element of F₁()
y is Element of F₂()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F₄(x,y) is Element of F₃()
x is Element of F₁()
y is Element of F₂()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F₅(x,y) is Element of F₃()
x is Element of F₁()
y is Element of F₂()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F₆(x,y) is Element of F₃()
x is Element of F₁()
y is Element of F₂()
v is set
v is Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like Element of bool [:[:F₁(),F₂():],F₃():]
dom v is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
bool [:F₁(),F₂():] is set
c₄ is Element of F₁()
z is Element of F₂()
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
z is Element of F₁()
y is Element of F₂()
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
c₄ is Element of F₁()
z is Element of F₂()
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
v . [c₄,z] is set
F₄(c₄,z) is Element of F₃()
F₅(c₄,z) is Element of F₃()
F₆(c₄,z) is Element of F₃()
F₁() is set
F₂() is set
F₃() is set
[:F₁(),F₂():] is set
[:[:F₁(),F₂():],F₃():] is set
bool [:[:F₁(),F₂():],F₃():] is set
f is set
v is set
v is set
c₄ is set
[v,c₄] is set
{v,c₄} is set
{v} is set
{{v,c₄},{v}} is set
F₄(v,c₄) is set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
z is set
F₄(z,y) is set
F₅(z,y) is set
F₅(v,c₄) is set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
z is set
F₄(z,y) is set
F₅(z,y) is set
z is set
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
z is set
z is set
[z,z] is set
{z,z} is set
{z} is set
{{z,z},{z}} is set
v . [z,z] is set
F₄(z,z) is set
v . [z,z] is set
F₅(z,z) is set
v is set
v is Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like Element of bool [:[:F₁(),F₂():],F₃():]
dom v is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
bool [:F₁(),F₂():] is set
c₄ is set
z is set
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
c₄ is set
z is set
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
v . [c₄,z] is set
F₄(c₄,z) is set
F₅(c₄,z) is set
F₁() is set
F₂() is set
F₃() is set
[:F₁(),F₂():] is set
[:[:F₁(),F₂():],F₃():] is set
bool [:[:F₁(),F₂():],F₃():] is set
f is set
v is set
v is set
c₄ is set
[v,c₄] is set
{v,c₄} is set
{v} is set
{{v,c₄},{v}} is set
F₄(v,c₄) is set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
z is set
F₄(z,y) is set
F₅(z,y) is set
F₆(z,y) is set
F₅(v,c₄) is set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
z is set
F₄(z,y) is set
F₅(z,y) is set
F₆(z,y) is set
F₆(v,c₄) is set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
z is set
F₄(z,y) is set
F₅(z,y) is set
F₆(z,y) is set
z is set
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
c₄ is set
v . c₄ is set
z is set
z is set
[z,z] is set
{z,z} is set
{z} is set
{{z,z},{z}} is set
v . [z,z] is set
F₄(z,z) is set
v . [z,z] is set
F₅(z,z) is set
v . [z,z] is set
F₆(z,z) is set
v is set
v is Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like Element of bool [:[:F₁(),F₂():],F₃():]
dom v is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
bool [:F₁(),F₂():] is set
c₄ is set
z is set
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
c₄ is set
z is set
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
v . [c₄,z] is set
F₄(c₄,z) is set
F₅(c₄,z) is set
F₆(c₄,z) is set
F₂() is non empty set
F₁() is non empty set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is Element of F₁()
v is Element of F₁()
v is Element of F₁()
f is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom f is Element of bool F₁()
bool F₁() is set
v is set
c₄ is Element of F₁()
v is Relation-like F₁() -defined F₂() -valued Function-like V29(F₁(),F₂()) Element of bool [:F₁(),F₂():]
c₄ is Element of F₁()
v . c₄ is Element of F₂()
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₅(c₄) is Element of F₂()
F₂() is non empty set
F₁() is non empty set
[:F₁(),F₂():] is set
bool [:F₁(),F₂():] is set
f is Element of F₁()
v is Element of F₁()
v is Element of F₁()
c₄ is Element of F₁()
z is Element of F₁()
z is Element of F₁()
f is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom f is Element of bool F₁()
bool F₁() is set
v is set
c₄ is Element of F₁()
v is Relation-like F₁() -defined F₂() -valued Function-like V29(F₁(),F₂()) Element of bool [:F₁(),F₂():]
c₄ is Element of F₁()
v . c₄ is Element of F₂()
F₃(c₄) is Element of F₂()
F₄(c₄) is Element of F₂()
F₅(c₄) is Element of F₂()
F₆(c₄) is Element of F₂()
F₃() is non empty set
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is set
[:[:F₁(),F₂():],F₃():] is set
bool [:[:F₁(),F₂():],F₃():] is set
f is Element of F₁()
v is Element of F₂()
f is Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like Element of bool [:[:F₁(),F₂():],F₃():]
dom f is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
bool [:F₁(),F₂():] is set
v is Relation-like Function-like set
v is set
c₄ is set
z is set
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
y is Element of F₁()
z is Element of F₂()
v is Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like V29([:F₁(),F₂():],F₃()) Element of bool [:[:F₁(),F₂():],F₃():]
dom v is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
c₄ is Element of F₁()
z is Element of F₂()
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
v . [c₄,z] is set
F₄(c₄,z) is Element of F₃()
F₅(c₄,z) is Element of F₃()
F₃() is non empty set
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is set
[:[:F₁(),F₂():],F₃():] is set
bool [:[:F₁(),F₂():],F₃():] is set
f is Element of F₁()
v is Element of F₂()
v is Element of F₁()
c₄ is Element of F₂()
z is Element of F₁()
z is Element of F₂()
f is Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like Element of bool [:[:F₁(),F₂():],F₃():]
dom f is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
bool [:F₁(),F₂():] is set
v is Relation-like Function-like set
v is set
c₄ is set
z is set
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
y is Element of F₁()
z is Element of F₂()
v is Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like V29([:F₁(),F₂():],F₃()) Element of bool [:[:F₁(),F₂():],F₃():]
dom v is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
c₄ is Element of F₁()
z is Element of F₂()
[c₄,z] is set
{c₄,z} is set
{c₄} is set
{{c₄,z},{c₄}} is set
z is Element of F₁()
y is Element of F₂()
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
x is Element of F₁()
d is Element of F₂()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
v . [x,d] is set
F₄(x,d) is Element of F₃()
F₅(x,d) is Element of F₃()
F₆(x,d) is Element of F₃()