:: SCHEME1 semantic presentation

REAL is non empty set
NAT is non empty V18() V19() V20() Element of bool REAL

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 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 ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F1() . f is ext-real V25() V32() Element of REAL
f is ext-real V18() V19() V20() V24() V25() V32() set
F1() . 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
c4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F1() . c4 is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F1() . z is ext-real V25() V32() Element of REAL
v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c4 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
F1() . z is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() set
F1() . 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
F1() . x is ext-real V25() V32() Element of REAL
d is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F1() . d is ext-real V25() V32() Element of REAL

v is ext-real V18() V19() V20() V24() V25() V32() Element of NAT

v . 0 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
dom v is Element of bool NAT

rng v is V46() V47() V48() V51() Element of bool NAT

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
c4 . (z + 1) is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c4 . z 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
F1() . z is ext-real V25() V32() Element of REAL
z is ext-real V18() V19() V20() V24() V25() V32() set
F1() . 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
F1() . 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
F1() . y is ext-real V25() V32() Element of REAL
x is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F1() . 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
c10 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
z . c10 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
F1() . (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

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
F1() . d is ext-real V25() V32() Element of REAL
c10 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
F1() . c10 is ext-real V25() V32() Element of REAL
F1() . (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
F1() . 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

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
F1((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
F2(((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

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
c4 . (2 * z) is ext-real V25() V32() Element of REAL
F1(z) is ext-real V25() V32() Element of REAL
(2 * z) + 1 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c4 . ((2 * z) + 1) is ext-real V25() V32() Element of REAL
F2(z) is ext-real V25() V32() Element of REAL
(2 * z) / 2 is ext-real V25() V32() set
F1(((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
F2(((((2 * z) + 1) - 1) / 2)) is ext-real V25() V32() Element of REAL

f is Element of bool NAT
v is Element of bool NAT
v is Element of bool NAT
c4 is ext-real V18() V19() V20() V24() V25() V32() Element of NAT
c4 / 3 is ext-real V25() V32() set
F1((c4 / 3)) is ext-real V25() V32() Element of REAL
c4 - 1 is ext-real V25() V32() set
(c4 - 1) / 3 is ext-real V25() V32() set
F2(((c4 - 1) / 3)) is ext-real V25() V32() Element of REAL
c4 - 2 is ext-real V25() V32() set
(c4 - 2) / 3 is ext-real V25() V32() set
F3(((c4 - 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

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
F1(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
F2(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
F3(z) is ext-real V25() V32() Element of REAL
(3 * z) / 3 is ext-real V25() V32() set
F1(((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
F2(((((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
F3(((((3 * z) + 2) - 2) / 3)) is ext-real V25() V32() Element of REAL

f is Element of bool NAT
v is Element of bool NAT
v is Element of bool NAT
c4 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
F1((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
F2(((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
F3(((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
F4(((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

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
F1(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
F2(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
F3(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
F4(y) is ext-real V25() V32() Element of REAL
(4 * y) / 4 is ext-real V25() V32() set
F1(((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
F2(((((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
F3(((((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
F4(((((4 * y) + 3) - 3) / 4)) is ext-real V25() V32() Element of REAL

f is Element of bool NAT
v is Element of bool NAT
v is Element of bool NAT
c4 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
F1((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
F2(((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
F3(((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
F4(((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
F5(((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

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
F1(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
F2(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
F3(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
F4(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
F5(x) is ext-real V25() V32() Element of REAL
(5 * x) / 5 is ext-real V25() V32() set
F1(((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
F2(((((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
F3(((((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
F4(((((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
F5(((((5 * x) + 4) - 4) / 5)) is ext-real V25() V32() Element of REAL
F2() is non empty set
F1() is non empty set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is set
v is set
F3(v) is Element of F2()
F4(v) is Element of F2()
v is Element of F1()
v is Element of F1()
z is set

dom v is set
v is set
rng v is set
v is set
c4 is set
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
v is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom v is Element of bool F1()
bool F1() is set
c4 is Element of F1()
z is Element of F1()
c4 is Element of F1()
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F2() is non empty set
F1() is non empty set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is set
v is set
F3(v) is Element of F2()
F4(v) is Element of F2()
v is Element of F1()
F3(v) is Element of F2()
F4(v) is Element of F2()
z is set
v is Element of F1()
F4(v) is Element of F2()
F3(v) is Element of F2()
z is set
v is Element of F1()
z is set

dom v is set
v is set
rng v is set
v is set
c4 is set
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
v is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom v is Element of bool F1()
bool F1() is set
c4 is Element of F1()
z is Element of F1()
c4 is Element of F1()
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F2() is non empty set
F1() is non empty set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is Element of F1()
f is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom f is Element of bool F1()
bool F1() is set
v is set
v is Element of F1()
v is Element of F1()
f . v is set
F3(v) is Element of F2()
F4(v) is Element of F2()
F2() is non empty set
F1() is non empty set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is set
v is set
F3(v) is Element of F2()
F4(v) is Element of F2()
F5(v) is Element of F2()
v is Element of F1()
v is Element of F1()
v is Element of F1()
z is set

dom v is set
rng v is set
v is set
c4 is set
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F5(c4) is Element of F2()
v is set
v is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom v is Element of bool F1()
bool F1() is set
c4 is Element of F1()
z is Element of F1()
c4 is Element of F1()
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F5(c4) is Element of F2()
F2() is non empty set
F1() is non empty set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is set
v is set
F3(v) is Element of F2()
F4(v) is Element of F2()
F5(v) is Element of F2()
v is Element of F1()
F3(v) is Element of F2()
F4(v) is Element of F2()
F5(v) is Element of F2()
z is set
F5(v) is Element of F2()
z is set
z is set
v is Element of F1()
F3(v) is Element of F2()
F4(v) is Element of F2()
F5(v) is Element of F2()
z is set
F4(v) is Element of F2()
F5(v) is Element of F2()
z is set
z is set
v is Element of F1()
F3(v) is Element of F2()
F5(v) is Element of F2()
F4(v) is Element of F2()
z is set
F4(v) is Element of F2()
F5(v) is Element of F2()
z is set
z is set
v is Element of F1()
z is set

dom v is set
rng v is set
v is set
c4 is set
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F5(c4) is Element of F2()
v is set
v is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom v is Element of bool F1()
bool F1() is set
c4 is Element of F1()
z is Element of F1()
c4 is Element of F1()
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F5(c4) is Element of F2()
F2() is non empty set
F1() is non empty set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is set
v is set
F3(v) is Element of F2()
F4(v) is Element of F2()
F5(v) is Element of F2()
F6(v) is Element of F2()
v is Element of F1()
v is Element of F1()
v is Element of F1()
v is Element of F1()
z is set

dom v is set
rng v is set
v is set
c4 is set
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F5(c4) is Element of F2()
F6(c4) is Element of F2()
v is set
v is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom v is Element of bool F1()
bool F1() is set
c4 is Element of F1()
z is Element of F1()
c4 is Element of F1()
v . c4 is set
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F5(c4) is Element of F2()
F6(c4) is Element of F2()
F1() is set
F2() is set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is set
v is set
F3(v) is set
F4(v) is set
c4 is set

dom v is set
v is set
rng v is set
v is set
c4 is set
v . c4 is set
F3(c4) is set
F4(c4) is set
v is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom v is Element of bool F1()
bool F1() is set
c4 is set
z is set
c4 is set
v . c4 is set
F3(c4) is set
F4(c4) is set
F1() is set
F2() is set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is set
v is set
F3(v) is set
F4(v) is set
F5(v) is set
c4 is set

dom v is set
v is set
rng v is set
v is set
c4 is set
v . c4 is set
F3(c4) is set
F4(c4) is set
F5(c4) is set
v is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom v is Element of bool F1()
bool F1() is set
c4 is set
z is set
c4 is set
v . c4 is set
F3(c4) is set
F4(c4) is set
F5(c4) is set
F1() is set
F2() is set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is set
v is set
F3(v) is set
F4(v) is set
F5(v) is set
F6(v) is set
c4 is set

dom v is set
v is set
rng v is set
v is set
c4 is set
v . c4 is set
F3(c4) is set
F4(c4) is set
F5(c4) is set
F6(c4) is set
v is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom v is Element of bool F1()
bool F1() is set
c4 is set
z is set
c4 is set
v . c4 is set
F3(c4) is set
F4(c4) is set
F5(c4) is set
F6(c4) is set
F3() is non empty set
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is set
f is set
v is set
v is set
c4 is set
[v,c4] is set
{v,c4} is set
{v} is set
{{v,c4},{v}} is set
z is Element of F1()
z is Element of F2()
F4(z,z) is Element of F3()
x is Element of F1()
d is Element of F2()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F3()
F4(x,d) is Element of F3()
F5(x,d) is Element of F3()
z is Element of F1()
z is Element of F2()
F5(z,z) is Element of F3()
x is Element of F1()
d is Element of F2()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F3()
F4(x,d) is Element of F3()
F5(x,d) is Element of F3()
z is Element of F1()
z is Element of F2()
y is Element of F3()

dom v is set
rng v is set
v is set
c4 is set
v . c4 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 F1()
y is Element of F2()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F4(x,y) is Element of F3()
x is Element of F1()
y is Element of F2()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F5(x,y) is Element of F3()
x is Element of F1()
y is Element of F2()
v is set
v is Relation-like [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom v is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is set
c4 is Element of F1()
z is Element of F2()
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
z is Element of F1()
y is Element of F2()
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
c4 is Element of F1()
z is Element of F2()
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
v . [c4,z] is set
F4(c4,z) is Element of F3()
F5(c4,z) is Element of F3()
F3() is non empty set
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is set
f is set
v is set
v is set
c4 is set
[v,c4] is set
{v,c4} is set
{v} is set
{{v,c4},{v}} is set
z is Element of F1()
z is Element of F2()
F4(z,z) is Element of F3()
x is Element of F1()
d is Element of F2()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F3()
F4(x,d) is Element of F3()
F5(x,d) is Element of F3()
F6(x,d) is Element of F3()
z is Element of F1()
z is Element of F2()
F5(z,z) is Element of F3()
x is Element of F1()
d is Element of F2()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F3()
F4(x,d) is Element of F3()
F5(x,d) is Element of F3()
F6(x,d) is Element of F3()
z is Element of F1()
z is Element of F2()
F6(z,z) is Element of F3()
x is Element of F1()
d is Element of F2()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
y is Element of F3()
F4(x,d) is Element of F3()
F5(x,d) is Element of F3()
F6(x,d) is Element of F3()
z is Element of F1()
z is Element of F2()
y is Element of F3()

dom v is set
rng v is set
v is set
c4 is set
v . c4 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 F1()
y is Element of F2()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F4(x,y) is Element of F3()
x is Element of F1()
y is Element of F2()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F5(x,y) is Element of F3()
x is Element of F1()
y is Element of F2()
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
v . [x,y] is set
F6(x,y) is Element of F3()
x is Element of F1()
y is Element of F2()
v is set
v is Relation-like [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom v is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is set
c4 is Element of F1()
z is Element of F2()
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
z is Element of F1()
y is Element of F2()
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
c4 is Element of F1()
z is Element of F2()
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
v . [c4,z] is set
F4(c4,z) is Element of F3()
F5(c4,z) is Element of F3()
F6(c4,z) is Element of F3()
F1() is set
F2() is set
F3() is set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is set
f is set
v is set
v is set
c4 is set
[v,c4] is set
{v,c4} is set
{v} is set
{{v,c4},{v}} is set
F4(v,c4) 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
F4(z,y) is set
F5(z,y) is set
F5(v,c4) 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
F4(z,y) is set
F5(z,y) is set
z is set

dom v is set
rng v is set
v is set
c4 is set
v . c4 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
F4(z,z) is set
v . [z,z] is set
F5(z,z) is set
v is set
v is Relation-like [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom v is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is set
c4 is set
z is set
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
c4 is set
z is set
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
v . [c4,z] is set
F4(c4,z) is set
F5(c4,z) is set
F1() is set
F2() is set
F3() is set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is set
f is set
v is set
v is set
c4 is set
[v,c4] is set
{v,c4} is set
{v} is set
{{v,c4},{v}} is set
F4(v,c4) 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
F4(z,y) is set
F5(z,y) is set
F6(z,y) is set
F5(v,c4) 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
F4(z,y) is set
F5(z,y) is set
F6(z,y) is set
F6(v,c4) 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
F4(z,y) is set
F5(z,y) is set
F6(z,y) is set
z is set

dom v is set
rng v is set
v is set
c4 is set
v . c4 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
F4(z,z) is set
v . [z,z] is set
F5(z,z) is set
v . [z,z] is set
F6(z,z) is set
v is set
v is Relation-like [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom v is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is set
c4 is set
z is set
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
c4 is set
z is set
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
v . [c4,z] is set
F4(c4,z) is set
F5(c4,z) is set
F6(c4,z) is set
F2() is non empty set
F1() is non empty set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is Element of F1()
v is Element of F1()
v is Element of F1()
f is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom f is Element of bool F1()
bool F1() is set
v is set
c4 is Element of F1()
v is Relation-like F1() -defined F2() -valued Function-like V29(F1(),F2()) Element of bool [:F1(),F2():]
c4 is Element of F1()
v . c4 is Element of F2()
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F5(c4) is Element of F2()
F2() is non empty set
F1() is non empty set
[:F1(),F2():] is set
bool [:F1(),F2():] is set
f is Element of F1()
v is Element of F1()
v is Element of F1()
c4 is Element of F1()
z is Element of F1()
z is Element of F1()
f is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom f is Element of bool F1()
bool F1() is set
v is set
c4 is Element of F1()
v is Relation-like F1() -defined F2() -valued Function-like V29(F1(),F2()) Element of bool [:F1(),F2():]
c4 is Element of F1()
v . c4 is Element of F2()
F3(c4) is Element of F2()
F4(c4) is Element of F2()
F5(c4) is Element of F2()
F6(c4) is Element of F2()
F3() is non empty set
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is set
f is Element of F1()
v is Element of F2()
f is Relation-like [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom f is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is set

v is set
c4 is set
z is set
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
y is Element of F1()
z is Element of F2()
v is Relation-like [:F1(),F2():] -defined F3() -valued Function-like V29([:F1(),F2():],F3()) Element of bool [:[:F1(),F2():],F3():]
dom v is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
c4 is Element of F1()
z is Element of F2()
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
v . [c4,z] is set
F4(c4,z) is Element of F3()
F5(c4,z) is Element of F3()
F3() is non empty set
F1() is non empty set
F2() is non empty set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is set
f is Element of F1()
v is Element of F2()
v is Element of F1()
c4 is Element of F2()
z is Element of F1()
z is Element of F2()
f is Relation-like [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom f is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is set

v is set
c4 is set
z is set
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
y is Element of F1()
z is Element of F2()
v is Relation-like [:F1(),F2():] -defined F3() -valued Function-like V29([:F1(),F2():],F3()) Element of bool [:[:F1(),F2():],F3():]
dom v is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
c4 is Element of F1()
z is Element of F2()
[c4,z] is set
{c4,z} is set
{c4} is set
{{c4,z},{c4}} is set
z is Element of F1()
y is Element of F2()
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
x is Element of F1()
d is Element of F2()
[x,d] is set
{x,d} is set
{x} is set
{{x,d},{x}} is set
v . [x,d] is set
F4(x,d) is Element of F3()
F5(x,d) is Element of F3()
F6(x,d) is Element of F3()