:: RECDEF_2 semantic presentation

REAL is set
NAT is non empty V24() V25() V26() Element of bool REAL
bool REAL is non empty set
COMPLEX is set
RAT is set
INT is set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty set
[:[:NAT,NAT:],NAT:] is non empty set
bool [:[:NAT,NAT:],NAT:] is non empty set
NAT is non empty V24() V25() V26() set
bool NAT is non empty set
bool NAT is non empty set
K285() is set
1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
{} is set
the empty ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() set is empty ext-real non negative V24() V25() V26() V28() V29() V30() V31() V32() V33() set
0 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
3 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
4 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
x is V1() triple set
y is set
X is set
Y is set
[y,X,Y] is V1() triple set
[y,X] is V1() set
{y,X} is set
{y} is set
{{y,X},{y}} is set
[[y,X],Y] is V1() set
{[y,X],Y} is set
{[y,X]} is set
{{[y,X],Y},{[y,X]}} is set
[y,X,Y] `1_3 is set
[y,X,Y] `1 is set
([y,X,Y] `1) `1 is set
[y,X,Y] `2_3 is set
([y,X,Y] `1) `2 is set
[y,X,Y] `2 is set
x `1_3 is set
x `1 is set
(x `1) `1 is set
Z is set
f is set
x is set
f3 is set
[f,x,f3] is V1() triple set
[f,x] is V1() set
{f,x} is set
{f} is set
{{f,x},{f}} is set
[[f,x],f3] is V1() set
{[f,x],f3} is set
{[f,x]} is set
{{[f,x],f3},{[f,x]}} is set
f is set
x `2_3 is set
(x `1) `2 is set
Z is set
f is set
x is set
f3 is set
[f,x,f3] is V1() triple set
[f,x] is V1() set
{f,x} is set
{f} is set
{{f,x},{f}} is set
[[f,x],f3] is V1() set
{[f,x],f3} is set
{[f,x]} is set
{{[f,x],f3},{[f,x]}} is set
f is set
x `2 is set
Z is set
f is set
x is set
f3 is set
[f,x,f3] is V1() triple set
[f,x] is V1() set
{f,x} is set
{f} is set
{{f,x},{f}} is set
[[f,x],f3] is V1() set
{[f,x],f3} is set
{[f,x]} is set
{{[f,x],f3},{[f,x]}} is set
f is set
x is set
x `1_3 is set
x `1 is set
(x `1) `1 is set
x `2_3 is set
(x `1) `2 is set
x `2 is set
[(x `1_3),(x `2_3),(x `2)] is V1() triple set
[(x `1_3),(x `2_3)] is V1() set
{(x `1_3),(x `2_3)} is set
{(x `1_3)} is set
{{(x `1_3),(x `2_3)},{(x `1_3)}} is set
[[(x `1_3),(x `2_3)],(x `2)] is V1() set
{[(x `1_3),(x `2_3)],(x `2)} is set
{[(x `1_3),(x `2_3)]} is set
{{[(x `1_3),(x `2_3)],(x `2)},{[(x `1_3),(x `2_3)]}} is set
y is set
X is set
Y is set
[y,X,Y] is V1() triple set
[y,X] is V1() set
{y,X} is set
{y} is set
{{y,X},{y}} is set
[[y,X],Y] is V1() set
{[y,X],Y} is set
{[y,X]} is set
{{[y,X],Y},{[y,X]}} is set
x is set
x `1_3 is set
x `1 is set
(x `1) `1 is set
x `2_3 is set
(x `1) `2 is set
x `2 is set
y is set
X is set
Y is set
[:y,X,Y:] is set
Z is Element of y
f is Element of X
x is Element of Y
[Z,f,x] is V1() triple set
[Z,f] is V1() set
{Z,f} is set
{Z} is set
{{Z,f},{Z}} is set
[[Z,f],x] is V1() set
{[Z,f],x} is set
{[Z,f]} is set
{{[Z,f],x},{[Z,f]}} is set
x is set
x `1_3 is set
x `1 is set
(x `1) `1 is set
x `2_3 is set
(x `1) `2 is set
x `2 is set
[(x `1_3),(x `2_3),(x `2)] is V1() triple set
[(x `1_3),(x `2_3)] is V1() set
{(x `1_3),(x `2_3)} is set
{(x `1_3)} is set
{{(x `1_3),(x `2_3)},{(x `1_3)}} is set
[[(x `1_3),(x `2_3)],(x `2)] is V1() set
{[(x `1_3),(x `2_3)],(x `2)} is set
{[(x `1_3),(x `2_3)]} is set
{{[(x `1_3),(x `2_3)],(x `2)},{[(x `1_3),(x `2_3)]}} is set
y is set
X is set
Y is set
[:y,X,Y:] is set
Z is Element of y
f is Element of X
x is Element of Y
[Z,f,x] is V1() triple set
[Z,f] is V1() set
{Z,f} is set
{Z} is set
{{Z,f},{Z}} is set
[[Z,f],x] is V1() set
{[Z,f],x} is set
{[Z,f]} is set
{{[Z,f],x},{[Z,f]}} is set
x is V1() triple quadruple set
y is set
X is set
Y is set
Z is set
[y,X,Y,Z] is V1() triple quadruple set
[y,X,Y] is V1() triple set
[y,X] is V1() set
{y,X} is set
{y} is set
{{y,X},{y}} is set
[[y,X],Y] is V1() set
{[y,X],Y} is set
{[y,X]} is set
{{[y,X],Y},{[y,X]}} is set
[[y,X,Y],Z] is V1() set
{[y,X,Y],Z} is set
{[y,X,Y]} is set
{{[y,X,Y],Z},{[y,X,Y]}} is set
[y,X,Y,Z] `1_4 is set
[y,X,Y,Z] `1 is set
([y,X,Y,Z] `1) `1 is set
(([y,X,Y,Z] `1) `1) `1 is set
[y,X,Y,Z] `2_4 is set
(([y,X,Y,Z] `1) `1) `2 is set
[y,X,Y,Z] `2_3 is set
([y,X,Y,Z] `1) `2 is set
[y,X,Y,Z] `2 is set
x `1_4 is set
x `1 is set
(x `1) `1 is set
((x `1) `1) `1 is set
f is set
x is set
f3 is set
f is set
c is set
[x,f3,f,c] is V1() triple quadruple set
[x,f3,f] is V1() triple set
[x,f3] is V1() set
{x,f3} is set
{x} is set
{{x,f3},{x}} is set
[[x,f3],f] is V1() set
{[x,f3],f} is set
{[x,f3]} is set
{{[x,f3],f},{[x,f3]}} is set
[[x,f3,f],c] is V1() set
{[x,f3,f],c} is set
{[x,f3,f]} is set
{{[x,f3,f],c},{[x,f3,f]}} is set
c₁₁ is set
x `2_4 is set
((x `1) `1) `2 is set
f is set
x is set
f3 is set
f is set
c is set
[x,f3,f,c] is V1() triple quadruple set
[x,f3,f] is V1() triple set
[x,f3] is V1() set
{x,f3} is set
{x} is set
{{x,f3},{x}} is set
[[x,f3],f] is V1() set
{[x,f3],f} is set
{[x,f3]} is set
{{[x,f3],f},{[x,f3]}} is set
[[x,f3,f],c] is V1() set
{[x,f3,f],c} is set
{[x,f3,f]} is set
{{[x,f3,f],c},{[x,f3,f]}} is set
c₁₁ is set
x `2_3 is set
(x `1) `2 is set
f is set
x is set
f3 is set
f is set
c is set
[x,f3,f,c] is V1() triple quadruple set
[x,f3,f] is V1() triple set
[x,f3] is V1() set
{x,f3} is set
{x} is set
{{x,f3},{x}} is set
[[x,f3],f] is V1() set
{[x,f3],f} is set
{[x,f3]} is set
{{[x,f3],f},{[x,f3]}} is set
[[x,f3,f],c] is V1() set
{[x,f3,f],c} is set
{[x,f3,f]} is set
{{[x,f3,f],c},{[x,f3,f]}} is set
c<sub>11</sub> is set
x `2 is set
f is set
x is set
f3 is set
f is set
c is set
[x,f3,f,c] is V1() triple quadruple set
[x,f3,f] is V1() triple set
[x,f3] is V1() set
{x,f3} is set
{x} is set
{{x,f3},{x}} is set
[[x,f3],f] is V1() set
{[x,f3],f} is set
{[x,f3]} is set
{{[x,f3],f},{[x,f3]}} is set
[[x,f3,f],c] is V1() set
{[x,f3,f],c} is set
{[x,f3,f]} is set
{{[x,f3,f],c},{[x,f3,f]}} is set
c₁₁ is set
x is set
x `1_4 is set
x `1 is set
(x `1) `1 is set
((x `1) `1) `1 is set
x `2_4 is set
((x `1) `1) `2 is set
x `2_3 is set
(x `1) `2 is set
x `2 is set
[(x `1_4),(x `2_4),(x `2_3),(x `2)] is V1() triple quadruple set
[(x `1_4),(x `2_4),(x `2_3)] is V1() triple set
[(x `1_4),(x `2_4)] is V1() set
{(x `1_4),(x `2_4)} is set
{(x `1_4)} is set
{{(x `1_4),(x `2_4)},{(x `1_4)}} is set
[[(x `1_4),(x `2_4)],(x `2_3)] is V1() set
{[(x `1_4),(x `2_4)],(x `2_3)} is set
{[(x `1_4),(x `2_4)]} is set
{{[(x `1_4),(x `2_4)],(x `2_3)},{[(x `1_4),(x `2_4)]}} is set
[[(x `1_4),(x `2_4),(x `2_3)],(x `2)] is V1() set
{[(x `1_4),(x `2_4),(x `2_3)],(x `2)} is set
{[(x `1_4),(x `2_4),(x `2_3)]} is set
{{[(x `1_4),(x `2_4),(x `2_3)],(x `2)},{[(x `1_4),(x `2_4),(x `2_3)]}} is set
y is set
X is set
Y is set
Z is set
[y,X,Y,Z] is V1() triple quadruple set
[y,X,Y] is V1() triple set
[y,X] is V1() set
{y,X} is set
{y} is set
{{y,X},{y}} is set
[[y,X],Y] is V1() set
{[y,X],Y} is set
{[y,X]} is set
{{[y,X],Y},{[y,X]}} is set
[[y,X,Y],Z] is V1() set
{[y,X,Y],Z} is set
{[y,X,Y]} is set
{{[y,X,Y],Z},{[y,X,Y]}} is set
x is set
x `1_4 is set
x `1 is set
(x `1) `1 is set
((x `1) `1) `1 is set
x `2_4 is set
((x `1) `1) `2 is set
x `2_3 is set
(x `1) `2 is set
x `2 is set
y is set
X is set
Y is set
Z is set
[:y,X,Y,Z:] is set
f is Element of y
x is Element of X
f3 is Element of Y
f is Element of Z
[f,x,f3,f] is V1() triple quadruple set
[f,x,f3] is V1() triple set
[f,x] is V1() set
{f,x} is set
{f} is set
{{f,x},{f}} is set
[[f,x],f3] is V1() set
{[f,x],f3} is set
{[f,x]} is set
{{[f,x],f3},{[f,x]}} is set
[[f,x,f3],f] is V1() set
{[f,x,f3],f} is set
{[f,x,f3]} is set
{{[f,x,f3],f},{[f,x,f3]}} is set
x is set
x `1_4 is set
x `1 is set
(x `1) `1 is set
((x `1) `1) `1 is set
x `2_4 is set
((x `1) `1) `2 is set
x `2_3 is set
(x `1) `2 is set
x `2 is set
[(x `1_4),(x `2_4),(x `2_3),(x `2)] is V1() triple quadruple set
[(x `1_4),(x `2_4),(x `2_3)] is V1() triple set
[(x `1_4),(x `2_4)] is V1() set
{(x `1_4),(x `2_4)} is set
{(x `1_4)} is set
{{(x `1_4),(x `2_4)},{(x `1_4)}} is set
[[(x `1_4),(x `2_4)],(x `2_3)] is V1() set
{[(x `1_4),(x `2_4)],(x `2_3)} is set
{[(x `1_4),(x `2_4)]} is set
{{[(x `1_4),(x `2_4)],(x `2_3)},{[(x `1_4),(x `2_4)]}} is set
[[(x `1_4),(x `2_4),(x `2_3)],(x `2)] is V1() set
{[(x `1_4),(x `2_4),(x `2_3)],(x `2)} is set
{[(x `1_4),(x `2_4),(x `2_3)]} is set
{{[(x `1_4),(x `2_4),(x `2_3)],(x `2)},{[(x `1_4),(x `2_4),(x `2_3)]}} is set
y is set
X is set
Y is set
Z is set
[:y,X,Y,Z:] is set
f is Element of y
x is Element of X
f3 is Element of Y
f is Element of Z
[f,x,f3,f] is V1() triple quadruple set
[f,x,f3] is V1() triple set
[f,x] is V1() set
{f,x} is set
{f} is set
{{f,x},{f}} is set
[[f,x],f3] is V1() set
{[f,x],f3} is set
{[f,x]} is set
{{[f,x],f3},{[f,x]}} is set
[[f,x,f3],f] is V1() set
{[f,x,f3],f} is set
{[f,x,f3]} is set
{{[f,x,f3],f},{[f,x,f3]}} is set
F<sub>1</sub>() is set
x is set
y is set
X is Relation-like Function-like set
proj1 X is set
Y is set
Z is Relation-like Function-like set
proj1 Z is set
f is Relation-like Function-like set
proj1 f is set
X +* f is Relation-like Function-like set
(X +* f) +* Z is Relation-like Function-like set
proj1 ((X +* f) +* Z) is set
proj1 (X +* f) is set
(proj1 (X +* f)) \/ (proj1 Z) is set
(proj1 X) \/ (proj1 f) is set
((proj1 X) \/ (proj1 f)) \/ (proj1 Z) is set
f3 is set
f3 is set
f3 is set
x \/ Y is set
f3 is set
f3 is set
((X +* f) +* Z) . f3 is set
F<sub>2</sub>(f3) is set
F<sub>3</sub>(f3) is set
F<sub>4</sub>(f3) is set
(X +* f) . f3 is set
X . f3 is set
f . f3 is set
Z . f3 is set
F<sub>1</sub>() is set
x is set
y is set
X is Relation-like Function-like set
proj1 X is set
Y is set
Z is Relation-like Function-like set
proj1 Z is set
f is set
x is Relation-like Function-like set
proj1 x is set
f3 is Relation-like Function-like set
proj1 f3 is set
X +* Z is Relation-like Function-like set
(X +* Z) +* f3 is Relation-like Function-like set
((X +* Z) +* f3) +* x is Relation-like Function-like set
proj1 (((X +* Z) +* f3) +* x) is set
proj1 ((X +* Z) +* f3) is set
(proj1 ((X +* Z) +* f3)) \/ (proj1 x) is set
proj1 (X +* Z) is set
(proj1 (X +* Z)) \/ (proj1 f3) is set
((proj1 (X +* Z)) \/ (proj1 f3)) \/ (proj1 x) is set
(proj1 X) \/ (proj1 Z) is set
((proj1 X) \/ (proj1 Z)) \/ (proj1 f3) is set
(((proj1 X) \/ (proj1 Z)) \/ (proj1 f3)) \/ (proj1 x) is set
c is set
c is set
c is set
c is set
x \/ Y is set
(x \/ Y) \/ f is set
c is set
c is set
(((X +* Z) +* f3) +* x) . c is set
F<sub>2</sub>(c) is set
F<sub>3</sub>(c) is set
F<sub>4</sub>(c) is set
F<sub>5</sub>(c) is set
((X +* Z) +* f3) . c is set
(X +* Z) . c is set
X . c is set
Z . c is set
f3 . c is set
x . c is set
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty set
[:NAT,F<sub>1</sub>():] is non empty set
bool [:NAT,F<sub>1</sub>():] is non empty set
[:NAT,F<sub>2</sub>():] is non empty set
bool [:NAT,F<sub>2</sub>():] is non empty set
F<sub>3</sub>() is Element of F<sub>1</sub>()
F<sub>4</sub>() is Element of F<sub>2</sub>()
[:F<sub>1</sub>(),F<sub>2</sub>():] is non empty set
x is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
y is Element of [:F<sub>1</sub>(),F<sub>2</sub>():]
y `1 is set
y `2 is set
y `1 is Element of F₁()
y `2 is Element of F<sub>2</sub>()
X is Element of F<sub>1</sub>()
Y is Element of F<sub>2</sub>()
[X,Y] is V1() Element of [:F<sub>1</sub>(),F<sub>2</sub>():]
{X,Y} is set
{X} is set
{{X,Y},{X}} is set
[X,Y] `1 is set
[X,Y] `2 is set
[:NAT,[:F<sub>1</sub>(),F<sub>2</sub>():]:] is non empty set
bool [:NAT,[:F<sub>1</sub>(),F<sub>2</sub>():]:] is non empty set
[F<sub>3</sub>(),F<sub>4</sub>()] is V1() Element of [:F<sub>1</sub>(),F<sub>2</sub>():]
{F<sub>3</sub>(),F<sub>4</sub>()} is set
{F<sub>3</sub>()} is set
{{F<sub>3</sub>(),F<sub>4</sub>()},{F<sub>3</sub>()}} is set
x is Relation-like NAT -defined [:F<sub>1</sub>(),F<sub>2</sub>():] -valued Function-like V18( NAT ,[:F<sub>1</sub>(),F<sub>2</sub>():]) Element of bool [:NAT,[:F<sub>1</sub>(),F<sub>2</sub>():]:]
x . 0 is Element of [:F<sub>1</sub>(),F<sub>2</sub>():]
pr1 x is Relation-like NAT -defined F<sub>1</sub>() -valued Function-like V18( NAT ,F<sub>1</sub>()) Element of bool [:NAT,F<sub>1</sub>():]
(pr1 x) . 0 is Element of F<sub>1</sub>()
pr2 x is Relation-like NAT -defined F<sub>2</sub>() -valued Function-like V18( NAT ,F<sub>2</sub>()) Element of bool [:NAT,F<sub>2</sub>():]
(pr2 x) . 0 is Element of F<sub>2</sub>()
[F<sub>3</sub>(),F<sub>4</sub>()] `1 is Element of F₁()
[F₃(),F₄()] `2 is Element of F<sub>2</sub>()
y is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(pr1 x) . y is Element of F<sub>1</sub>()
(pr2 x) . y is Element of F<sub>2</sub>()
y + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(pr1 x) . (y + 1) is Element of F<sub>1</sub>()
(pr2 x) . (y + 1) is Element of F<sub>2</sub>()
x . (y + 1) is Element of [:F<sub>1</sub>(),F<sub>2</sub>():]
(x . (y + 1)) `1 is Element of F₁()
(x . (y + 1)) `2 is Element of F<sub>2</sub>()
x . y is Element of [:F<sub>1</sub>(),F<sub>2</sub>():]
(x . y) `1 is Element of F₁()
(x . y) `2 is Element of F<sub>2</sub>()
F<sub>1</sub>() is set
F<sub>2</sub>() is set
F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>()) is set
F<sub>3</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())) is set
[F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>()),F<sub>3</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>()))] is V1() triple set
[F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())] is V1() set
{F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())} is set
{F<sub>2</sub>()} is set
{{F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())},{F<sub>2</sub>()}} is set
[[F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())],F<sub>3</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>()))] is V1() set
{[F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())],F<sub>3</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>()))} is set
{[F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())]} is set
{{[F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())],F<sub>3</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>()))},{[F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())]}} is set
X is Relation-like Function-like set
proj1 X is set
X . 0 is set
[F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())] is V1() triple set
[F<sub>1</sub>(),F<sub>2</sub>()] is V1() set
{F<sub>1</sub>(),F<sub>2</sub>()} is set
{F<sub>1</sub>()} is set
{{F<sub>1</sub>(),F<sub>2</sub>()},{F<sub>1</sub>()}} is set
[[F<sub>1</sub>(),F<sub>2</sub>()],F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())] is V1() set
{[F<sub>1</sub>(),F<sub>2</sub>()],F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())} is set
{[F<sub>1</sub>(),F<sub>2</sub>()]} is set
{{[F<sub>1</sub>(),F<sub>2</sub>()],F<sub>3</sub>(0,F<sub>1</sub>(),F<sub>2</sub>())},{[F<sub>1</sub>(),F<sub>2</sub>()]}} is set
Y is Relation-like Function-like set
proj1 Y is set
Z is Relation-like Function-like set
proj1 Z is set
Y . 0 is set
f is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . (f + 2) is set
f + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . (f + 1) is set
(Y . (f + 1)) `2_3 is set
(Y . (f + 1)) `1 is set
((Y . (f + 1)) `1) `2 is set
(Y . (f + 1)) `2 is set
(f + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F₃(((f + 1) + 1),((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)) is set
[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2),F₃(((f + 1) + 1),((Y . (f + 1)) `2_3),((Y . (f + 1)) `2))] is V1() triple set
[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)] is V1() set
{((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)} is set
{((Y . (f + 1)) `2_3)} is set
{{((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)},{((Y . (f + 1)) `2_3)}} is set
[[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)],F₃(((f + 1) + 1),((Y . (f + 1)) `2_3),((Y . (f + 1)) `2))] is V1() set
{[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)],F₃(((f + 1) + 1),((Y . (f + 1)) `2_3),((Y . (f + 1)) `2))} is set
{[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)]} is set
{{[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)],F₃(((f + 1) + 1),((Y . (f + 1)) `2_3),((Y . (f + 1)) `2))},{[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)]}} is set
(f + 2) - 1 is ext-real V31() V32() V33() set
2 - 1 is ext-real V31() V32() V33() set
f + (2 - 1) is ext-real V31() V32() V33() set
(f + 1) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
X . ((f + 1) -' 1) is set
X . f is set
(f + 2) -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
X . ((f + 2) -' 1) is set
X . (f + 1) is set
0 + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . (0 + 2) is set
(Y . (0 + 2)) `2_3 is set
(Y . (0 + 2)) `1 is set
((Y . (0 + 2)) `1) `2 is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . (0 + 1) is set
(Y . (0 + 1)) `2_3 is set
(Y . (0 + 1)) `1 is set
((Y . (0 + 1)) `1) `2 is set
(Y . (0 + 1)) `2 is set
(0 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F<sub>3</sub>(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)) is set
[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F<sub>3</sub>(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))] is V1() triple set
[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)] is V1() set
{((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)} is set
{((Y . (0 + 1)) `2_3)} is set
{{((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)},{((Y . (0 + 1)) `2_3)}} is set
[[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)],F<sub>3</sub>(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))] is V1() set
{[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)],F<sub>3</sub>(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))} is set
{[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)]} is set
{{[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)],F<sub>3</sub>(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))},{[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)]}} is set
H<sub>1</sub>(0 + 1,Y . (0 + 1)) `2_3 is set
[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F₃(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))] `1 is set
([((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F<sub>3</sub>(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))] `1) `2 is set
Z . 0 is set
Z . 1 is set
(Y . 0) `1_3 is set
(Y . 0) `1 is set
((Y . 0) `1) `1 is set
Y . 1 is set
1 -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
X . (1 -' 1) is set
(Y . (0 + 1)) `1_3 is set
((Y . (0 + 1)) `1) `1 is set
(Y . 0) `2_3 is set
((Y . 0) `1) `2 is set
f is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . (f + 2) is set
f + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . (f + 1) is set
(Y . (f + 1)) `2_3 is set
(Y . (f + 1)) `1 is set
((Y . (f + 1)) `1) `2 is set
(Y . (f + 1)) `1_3 is set
((Y . (f + 1)) `1) `1 is set
Y . f is set
(Y . f) `2_3 is set
(Y . f) `1 is set
((Y . f) `1) `2 is set
Y . (f + 2) is set
(Y . (f + 2)) `1_3 is set
(Y . (f + 2)) `1 is set
((Y . (f + 2)) `1) `1 is set
(Y . f) `2 is set
(Y . (f + 2)) `2_3 is set
((Y . (f + 2)) `1) `2 is set
(Y . (f + 1)) `2 is set
Z . f is set
Z . (f + 1) is set
F<sub>3</sub>(f,(Z . f),(Z . (f + 1))) is set
(f + 1) + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . ((f + 1) + 2) is set
(f + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . ((f + 1) + 1) is set
(Y . ((f + 1) + 1)) `2_3 is set
(Y . ((f + 1) + 1)) `1 is set
((Y . ((f + 1) + 1)) `1) `2 is set
(Y . ((f + 1) + 1)) `1_3 is set
((Y . ((f + 1) + 1)) `1) `1 is set
Y . ((f + 1) + 2) is set
(Y . ((f + 1) + 2)) `1_3 is set
(Y . ((f + 1) + 2)) `1 is set
((Y . ((f + 1) + 2)) `1) `1 is set
(Y . ((f + 1) + 2)) `2_3 is set
((Y . ((f + 1) + 2)) `1) `2 is set
(Y . ((f + 1) + 1)) `2 is set
Z . ((f + 1) + 1) is set
F₃((f + 1),(Z . (f + 1)),(Z . ((f + 1) + 1))) is set
((f + 1) + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F₃((((f + 1) + 1) + 1),((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)) is set
[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F₃((((f + 1) + 1) + 1),((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2))] is V1() triple set
[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)] is V1() set
{((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)} is set
{((Y . ((f + 1) + 1)) `2_3)} is set
{{((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)},{((Y . ((f + 1) + 1)) `2_3)}} is set
[[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)],F₃((((f + 1) + 1) + 1),((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2))] is V1() set
{[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)],F₃((((f + 1) + 1) + 1),((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2))} is set
{[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)]} is set
{{[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)],F₃((((f + 1) + 1) + 1),((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2))},{[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)]}} is set
H₁((f + 1) + 1,Y . ((f + 1) + 1)) `1_3 is set
[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F<sub>3</sub>((((f + 1) + 1) + 1),((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2))] `1 is set
([((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F₃((((f + 1) + 1) + 1),((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2))] `1) `1 is set
H₁((f + 1) + 1,Y . ((f + 1) + 1)) `2_3 is set
([((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F<sub>3</sub>((((f + 1) + 1) + 1),((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2))] `1) `2 is set
1 + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . (1 + 2) is set
(Y . (1 + 2)) `1_3 is set
(Y . (1 + 2)) `1 is set
((Y . (1 + 2)) `1) `1 is set
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . (1 + 1) is set
(Y . (1 + 1)) `2_3 is set
(Y . (1 + 1)) `1 is set
((Y . (1 + 1)) `1) `2 is set
(Y . (1 + 1)) `2 is set
(1 + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F₃(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)) is set
[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2),F₃(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))] is V1() triple set
[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)] is V1() set
{((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)} is set
{((Y . (1 + 1)) `2_3)} is set
{{((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)},{((Y . (1 + 1)) `2_3)}} is set
[[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)],F₃(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))] is V1() set
{[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)],F₃(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))} is set
{[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)]} is set
{{[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)],F₃(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))},{[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)]}} is set
H₁(1 + 1,Y . (1 + 1)) `1_3 is set
[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2),F<sub>3</sub>(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))] `1 is set
([((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2),F₃(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))] `1) `1 is set
(Y . 0) `2 is set
F<sub>3</sub>((0 + 1),F<sub>2</sub>(),((Y . 0) `2)) is set
f -' 1 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f -' 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 - 1 is ext-real V31() V32() V33() set
f - 1 is ext-real V31() V32() V33() set
(f - 1) + 2 is ext-real V31() V32() V33() set
Y . ((f -' 1) + 1) is set
(Y . ((f -' 1) + 1)) `2_3 is set
(Y . ((f -' 1) + 1)) `1 is set
((Y . ((f -' 1) + 1)) `1) `2 is set
(Y . ((f -' 1) + 1)) `2 is set
((f -' 1) + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F<sub>3</sub>((((f -' 1) + 1) + 1),((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)) is set
[((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2),F<sub>3</sub>((((f -' 1) + 1) + 1),((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2))] is V1() triple set
[((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)] is V1() set
{((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)} is set
{((Y . ((f -' 1) + 1)) `2_3)} is set
{{((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)},{((Y . ((f -' 1) + 1)) `2_3)}} is set
[[((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)],F<sub>3</sub>((((f -' 1) + 1) + 1),((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2))] is V1() set
{[((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)],F<sub>3</sub>((((f -' 1) + 1) + 1),((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2))} is set
{[((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)]} is set
{{[((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)],F<sub>3</sub>((((f -' 1) + 1) + 1),((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2))},{[((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)]}} is set
H<sub>1</sub>((f -' 1) + 1,Y . ((f -' 1) + 1)) `2 is set
Z . (0 + 2) is set
(Y . (0 + 2)) `1_3 is set
((Y . (0 + 2)) `1) `1 is set
H<sub>1</sub>(0 + 1,Y . (0 + 1)) `1_3 is set
([((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F₃(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))] `1) `1 is set
(Y . 1) `1_3 is set
(Y . 1) `1 is set
((Y . 1) `1) `1 is set
(Y . 1) `2_3 is set
((Y . 1) `1) `2 is set
(Y . 0) `2 is set
Z . (0 + 1) is set
F₃(0,(Z . 0),(Z . (0 + 1))) is set
f is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . (f + 2) is set
Z . f is set
f + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . (f + 1) is set
F₃(f,(Z . f),(Z . (f + 1))) is set
F₁() is non empty set
[:NAT,F₁():] is non empty set
bool [:NAT,F₁():] is non empty set
F₂() is Element of F₁()
F₃() is Element of F₁()
x is Relation-like Function-like set
proj1 x is set
x . 0 is set
x . 1 is set
proj2 x is set
y is set
X is set
x . X is set
Y is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
1 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y - 2 is ext-real V31() V32() V33() set
(Y - 2) + 2 is ext-real V31() V32() V33() set
x . ((Y - 2) + 2) is set
x . (Y - 2) is set
(Y - 2) + 1 is ext-real V31() V32() V33() set
x . ((Y - 2) + 1) is set
F₄((Y - 2),(x . (Y - 2)),(x . ((Y - 2) + 1))) is Element of F₁()
Y is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F₃() is Relation-like Function-like set
proj1 F₃() is set
F₃() . 0 is set
F₁() is set
F₃() . 1 is set
F₂() is set
F₄() is Relation-like Function-like set
proj1 F₄() is set
F₄() . 0 is set
F₄() . 1 is set
x is set
F₃() . x is set
F₄() . x is set
x is ext-real non negative V24() V25() V26() V30() V31() V32() V33() set
F₃() . x is set
F₄() . x is set
x -' 2 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(x -' 2) + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F₃() . ((x -' 2) + 2) is set
F₃() . (x -' 2) is set
(x -' 2) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F₃() . ((x -' 2) + 1) is set
F₅((x -' 2),(F₃() . (x -' 2)),(F₃() . ((x -' 2) + 1))) is set
F₄() . ((x -' 2) + 2) is set
F₄() . (x -' 2) is set
F₄() . ((x -' 2) + 1) is set
F₅((x -' 2),(F₄() . (x -' 2)),(F₄() . ((x -' 2) + 1))) is set
(x -' 2) + 0 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F₁() is non empty set
[:NAT,F₁():] is non empty set
bool [:NAT,F₁():] is non empty set
F₄() is Relation-like NAT -defined F₁() -valued Function-like V18( NAT ,F₁()) Element of bool [:NAT,F₁():]
F₄() . 0 is Element of F₁()
F₂() is Element of F₁()
F₄() . 1 is Element of F₁()
F₃() is Element of F₁()
F₅() is Relation-like NAT -defined F₁() -valued Function-like V18( NAT ,F₁()) Element of bool [:NAT,F₁():]
F₅() . 0 is Element of F₁()
F₅() . 1 is Element of F₁()
proj1 F₅() is set
proj1 F₄() is set
F₁() is set
F₂() is set
F₃() is set
F₄(0,F₁(),F₂(),F₃()) is set
F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())) is set
F₄(2,F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))) is set
[F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())),F₄(2,F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())))] is V1() triple quadruple set
[F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))] is V1() triple set
[F₃(),F₄(0,F₁(),F₂(),F₃())] is V1() set
{F₃(),F₄(0,F₁(),F₂(),F₃())} is set
{F₃()} is set
{{F₃(),F₄(0,F₁(),F₂(),F₃())},{F₃()}} is set
[[F₃(),F₄(0,F₁(),F₂(),F₃())],F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))] is V1() set
{[F₃(),F₄(0,F₁(),F₂(),F₃())],F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))} is set
{[F₃(),F₄(0,F₁(),F₂(),F₃())]} is set
{{[F₃(),F₄(0,F₁(),F₂(),F₃())],F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))},{[F₃(),F₄(0,F₁(),F₂(),F₃())]}} is set
[[F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))],F₄(2,F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())))] is V1() set
{[F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))],F₄(2,F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())))} is set
{[F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))]} is set
{{[F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))],F₄(2,F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())))},{[F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))]}} is set
Y is Relation-like Function-like set
proj1 Y is set
Y . 0 is set
[F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))] is V1() triple quadruple set
[F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())] is V1() triple set
[F₂(),F₃()] is V1() set
{F₂(),F₃()} is set
{F₂()} is set
{{F₂(),F₃()},{F₂()}} is set
[[F₂(),F₃()],F₄(0,F₁(),F₂(),F₃())] is V1() set
{[F₂(),F₃()],F₄(0,F₁(),F₂(),F₃())} is set
{[F₂(),F₃()]} is set
{{[F₂(),F₃()],F₄(0,F₁(),F₂(),F₃())},{[F₂(),F₃()]}} is set
[[F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())],F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))] is V1() set
{[F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())],F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))} is set
{[F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())]} is set
{{[F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())],F₄(1,F₂(),F₃(),F₄(0,F₁(),F₂(),F₃()))},{[F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())]}} is set
[F₁(),F₂(),F₃(),F₄(0,F₁(),F₂(),F₃())] is V1() triple quadruple set
[F₁(),F₂(),F₃()] is V1() triple set
[F₁(),F₂()] is V1() set
{F₁(),F₂()} is set
{F₁()} is set
{{F₁(),F₂()},{F₁()}} is set
[[F₁(),F₂()],F₃()] is V1() set
{[F₁(),F₂()],F₃()} is set
{[F₁(),F₂()]} is set
{{[F₁(),F₂()],F₃()},{[F₁(),F₂()]}} is set
[[F₁(),F₂(),F₃()],F₄(0,F₁(),F₂(),F₃())] is V1() set
{[F₁(),F₂(),F₃()],F₄(0,F₁(),F₂(),F₃())} is set
{[F₁(),F₂(),F₃()]} is set
{{[F₁(),F₂(),F₃()],F₄(0,F₁(),F₂(),F₃())},{[F₁(),F₂(),F₃()]}} is set
Z is set
In (Z,NAT) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z is set
In (Z,NAT) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z is Relation-like Function-like set
proj1 Z is set
In (2,NAT) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . 2 is set
(In (2,NAT)) -' 2 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . ((In (2,NAT)) -' 2) is set
f is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f + 3 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . (f + 3) is set
f + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . (f + 2) is set
(Z . (f + 2)) `2_4 is set
(Z . (f + 2)) `1 is set
((Z . (f + 2)) `1) `1 is set
(((Z . (f + 2)) `1) `1) `2 is set
(Z . (f + 2)) `2_3 is set
((Z . (f + 2)) `1) `2 is set
(Z . (f + 2)) `2 is set
(f + 2) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F<sub>4</sub>(((f + 2) + 1),((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2)) is set
[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2),F<sub>4</sub>(((f + 2) + 1),((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2))] is V1() triple quadruple set
[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2)] is V1() triple set
[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3)] is V1() set
{((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3)} is set
{((Z . (f + 2)) `2_4)} is set
{{((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3)},{((Z . (f + 2)) `2_4)}} is set
[[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3)],((Z . (f + 2)) `2)] is V1() set
{[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3)],((Z . (f + 2)) `2)} is set
{[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3)]} is set
{{[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3)],((Z . (f + 2)) `2)},{[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3)]}} is set
[[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2)],F<sub>4</sub>(((f + 2) + 1),((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2))] is V1() set
{[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2)],F<sub>4</sub>(((f + 2) + 1),((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2))} is set
{[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2)]} is set
{{[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2)],F₄(((f + 2) + 1),((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2))},{[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2)]}} is set
In ((f + 2),NAT) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(In ((f + 2),NAT)) -' 2 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . ((In ((f + 2),NAT)) -' 2) is set
Y . f is set
In ((f + 3),NAT) is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(f + 3) - 2 is ext-real V31() V32() V33() set
3 - 2 is ext-real V31() V32() V33() set
f + (3 - 2) is ext-real V31() V32() V33() set
f + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(In ((f + 3),NAT)) -' 2 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Y . ((In ((f + 3),NAT)) -' 2) is set
Y . (f + 1) is set
Z . 1 is set
0 + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . (0 + 1) is set
(Z . (0 + 1)) `2_3 is set
(Z . (0 + 1)) `1 is set
((Z . (0 + 1)) `1) `2 is set
0 + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . (0 + 2) is set
(Z . (0 + 2)) `2_4 is set
(Z . (0 + 2)) `1 is set
((Z . (0 + 2)) `1) `1 is set
(((Z . (0 + 2)) `1) `1) `2 is set
Z . 0 is set
(Z . 0) `2_3 is set
(Z . 0) `1 is set
((Z . 0) `1) `2 is set
(Z . (0 + 1)) `2_4 is set
((Z . (0 + 1)) `1) `1 is set
(((Z . (0 + 1)) `1) `1) `2 is set
(Z . (0 + 1)) `2 is set
(Z . (0 + 2)) `2_3 is set
((Z . (0 + 2)) `1) `2 is set
(Z . 0) `2 is set
(Z . (0 + 1)) `1_4 is set
(((Z . (0 + 1)) `1) `1) `1 is set
(Z . 0) `2_4 is set
((Z . 0) `1) `1 is set
(((Z . 0) `1) `1) `2 is set
f is Relation-like Function-like set
proj1 f is set
0 + 3 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f . (0 + 3) is set
Z . (0 + 3) is set
(Z . (0 + 3)) `1_4 is set
(Z . (0 + 3)) `1 is set
((Z . (0 + 3)) `1) `1 is set
(((Z . (0 + 3)) `1) `1) `1 is set
(Z . (0 + 2)) `2 is set
(0 + 2) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F₄(((0 + 2) + 1),((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2)) is set
[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2),F₄(((0 + 2) + 1),((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2))] is V1() triple quadruple set
[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2)] is V1() triple set
[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3)] is V1() set
{((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3)} is set
{((Z . (0 + 2)) `2_4)} is set
{{((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3)},{((Z . (0 + 2)) `2_4)}} is set
[[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3)],((Z . (0 + 2)) `2)] is V1() set
{[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3)],((Z . (0 + 2)) `2)} is set
{[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3)]} is set
{{[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3)],((Z . (0 + 2)) `2)},{[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3)]}} is set
[[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2)],F₄(((0 + 2) + 1),((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2))] is V1() set
{[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2)],F₄(((0 + 2) + 1),((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2))} is set
{[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2)]} is set
{{[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2)],F<sub>4</sub>(((0 + 2) + 1),((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2))},{[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2)]}} is set
H<sub>1</sub>(0 + 2,Z . (0 + 2)) `1_4 is set
[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2),F<sub>4</sub>(((0 + 2) + 1),((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2))] `1 is set
([((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2),F₄(((0 + 2) + 1),((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2))] `1) `1 is set
(([((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2),F₄(((0 + 2) + 1),((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2))] `1) `1) `1 is set
f . 0 is set
f . 1 is set
f . 2 is set
(Z . 0) `1_4 is set
(((Z . 0) `1) `1) `1 is set
(Z . 1) `1_4 is set
(Z . 1) `1 is set
((Z . 1) `1) `1 is set
(((Z . 1) `1) `1) `1 is set
(Z . 2) `1_4 is set
(Z . 2) `1 is set
((Z . 2) `1) `1 is set
(((Z . 2) `1) `1) `1 is set
x is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
x + 3 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
f . (x + 3) is set
x + 2 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
Z . (x + 2) is set
(Z . (x + 2)) `2_4 is set
(Z . (x + 2)) `1 is set
((Z . (x + 2))