:: RECDEF_2 semantic presentation

REAL is set
NAT is non empty V24() V25() V26() Element of bool REAL
bool REAL is non empty set

RAT is set
INT is set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is non empty set
is non empty set
bool 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
c11 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
c11 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
c11 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
c11 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
F1() is set
x is set
y is set

proj1 X is set
Y is set

proj1 Z is set

proj1 f is set

(X +* f) +* Z is Relation-like Function-like set
proj1 ((X +* f) +* Z) is set
proj1 (X +* f) is set
(proj1 (X +* f)) \/ () is set
() \/ () is set
(() \/ ()) \/ () 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
F2(f3) is set
F3(f3) is set
F4(f3) is set
(X +* f) . f3 is set
X . f3 is set
f . f3 is set
Z . f3 is set
F1() is set
x is set
y is set

proj1 X is set
Y is set

proj1 Z is set
f is set

proj1 x is set

proj1 f3 is 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)) \/ () is set
proj1 (X +* Z) is set
(proj1 (X +* Z)) \/ (proj1 f3) is set
((proj1 (X +* Z)) \/ (proj1 f3)) \/ () is set
() \/ () is set
(() \/ ()) \/ (proj1 f3) is set
((() \/ ()) \/ (proj1 f3)) \/ () 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
F2(c) is set
F3(c) is set
F4(c) is set
F5(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
F1() is non empty set
F2() is non empty set
[:NAT,F1():] is non empty set
bool [:NAT,F1():] is non empty set
[:NAT,F2():] is non empty set
bool [:NAT,F2():] is non empty set
F3() is Element of F1()
F4() is Element of F2()
[:F1(),F2():] is non empty set
x is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
y is Element of [:F1(),F2():]
y `1 is set
y `2 is set
y `1 is Element of F1()
y `2 is Element of F2()
X is Element of F1()
Y is Element of F2()
[X,Y] is V1() Element of [:F1(),F2():]
{X,Y} is set
{X} is set
{{X,Y},{X}} is set
[X,Y] `1 is set
[X,Y] `2 is set
[:NAT,[:F1(),F2():]:] is non empty set
bool [:NAT,[:F1(),F2():]:] is non empty set
[F3(),F4()] is V1() Element of [:F1(),F2():]
{F3(),F4()} is set
{F3()} is set
{{F3(),F4()},{F3()}} is set
x is Relation-like NAT -defined [:F1(),F2():] -valued Function-like V18( NAT ,[:F1(),F2():]) Element of bool [:NAT,[:F1(),F2():]:]
x . 0 is Element of [:F1(),F2():]
pr1 x is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
(pr1 x) . 0 is Element of F1()
pr2 x is Relation-like NAT -defined F2() -valued Function-like V18( NAT ,F2()) Element of bool [:NAT,F2():]
(pr2 x) . 0 is Element of F2()
[F3(),F4()] `1 is Element of F1()
[F3(),F4()] `2 is Element of F2()
y is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
(pr1 x) . y is Element of F1()
(pr2 x) . y is Element of F2()
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 F1()
(pr2 x) . (y + 1) is Element of F2()
x . (y + 1) is Element of [:F1(),F2():]
(x . (y + 1)) `1 is Element of F1()
(x . (y + 1)) `2 is Element of F2()
x . y is Element of [:F1(),F2():]
(x . y) `1 is Element of F1()
(x . y) `2 is Element of F2()
F1() is set
F2() is set
F3(0,F1(),F2()) is set
F3(1,F2(),F3(0,F1(),F2())) is set
[F2(),F3(0,F1(),F2()),F3(1,F2(),F3(0,F1(),F2()))] is V1() triple set
[F2(),F3(0,F1(),F2())] is V1() set
{F2(),F3(0,F1(),F2())} is set
{F2()} is set
{{F2(),F3(0,F1(),F2())},{F2()}} is set
[[F2(),F3(0,F1(),F2())],F3(1,F2(),F3(0,F1(),F2()))] is V1() set
{[F2(),F3(0,F1(),F2())],F3(1,F2(),F3(0,F1(),F2()))} is set
{[F2(),F3(0,F1(),F2())]} is set
{{[F2(),F3(0,F1(),F2())],F3(1,F2(),F3(0,F1(),F2()))},{[F2(),F3(0,F1(),F2())]}} is set

proj1 X is set
X . 0 is set
[F1(),F2(),F3(0,F1(),F2())] is V1() triple set
[F1(),F2()] is V1() set
{F1(),F2()} is set
{F1()} is set
{{F1(),F2()},{F1()}} is set
[[F1(),F2()],F3(0,F1(),F2())] is V1() set
{[F1(),F2()],F3(0,F1(),F2())} is set
{[F1(),F2()]} is set
{{[F1(),F2()],F3(0,F1(),F2())},{[F1(),F2()]}} is set

proj1 Y is 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
F3(((f + 1) + 1),((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)) is set
[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2),F3(((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)],F3(((f + 1) + 1),((Y . (f + 1)) `2_3),((Y . (f + 1)) `2))] is V1() set
{[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)],F3(((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)],F3(((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
F3(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)) is set
[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F3(((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)],F3(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))] is V1() set
{[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)],F3(((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)],F3(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))},{[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)]}} is set
H1(0 + 1,Y . (0 + 1)) `2_3 is set
[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F3(((0 + 1) + 1),((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2))] `1 is set
([((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F3(((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
F3(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
F3((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
F3((((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),F3((((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)],F3((((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)],F3((((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)],F3((((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
H1((f + 1) + 1,Y . ((f + 1) + 1)) `1_3 is set
[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F3((((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),F3((((f + 1) + 1) + 1),((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2))] `1) `1 is set
H1((f + 1) + 1,Y . ((f + 1) + 1)) `2_3 is set
([((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F3((((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
F3(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)) is set
[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2),F3(((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)],F3(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))] is V1() set
{[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)],F3(((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)],F3(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))},{[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)]}} is set
H1(1 + 1,Y . (1 + 1)) `1_3 is set
[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2),F3(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))] `1 is set
([((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2),F3(((1 + 1) + 1),((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2))] `1) `1 is set
(Y . 0) `2 is set
F3((0 + 1),F2(),((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
F3((((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),F3((((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)],F3((((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)],F3((((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)],F3((((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
H1((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
H1(0 + 1,Y . (0 + 1)) `1_3 is set
([((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F3(((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
F3(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
F3(f,(Z . f),(Z . (f + 1))) is set
F1() is non empty set
[:NAT,F1():] is non empty set
bool [:NAT,F1():] is non empty set
F2() is Element of F1()
F3() is Element of F1()

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
F4((Y - 2),(x . (Y - 2)),(x . ((Y - 2) + 1))) is Element of F1()
Y is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

proj1 F3() is set
F3() . 0 is set
F1() is set
F3() . 1 is set
F2() is set

proj1 F4() is set
F4() . 0 is set
F4() . 1 is set
x is set
F3() . x is set
F4() . x is set
x is ext-real non negative V24() V25() V26() V30() V31() V32() V33() set
F3() . x is set
F4() . 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
F3() . ((x -' 2) + 2) is set
F3() . (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
F3() . ((x -' 2) + 1) is set
F5((x -' 2),(F3() . (x -' 2)),(F3() . ((x -' 2) + 1))) is set
F4() . ((x -' 2) + 2) is set
F4() . (x -' 2) is set
F4() . ((x -' 2) + 1) is set
F5((x -' 2),(F4() . (x -' 2)),(F4() . ((x -' 2) + 1))) is set
(x -' 2) + 0 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT
F1() is non empty set
[:NAT,F1():] is non empty set
bool [:NAT,F1():] is non empty set
F4() is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
F4() . 0 is Element of F1()
F2() is Element of F1()
F4() . 1 is Element of F1()
F3() is Element of F1()
F5() is Relation-like NAT -defined F1() -valued Function-like V18( NAT ,F1()) Element of bool [:NAT,F1():]
F5() . 0 is Element of F1()
F5() . 1 is Element of F1()
proj1 F5() is set
proj1 F4() is set
F1() is set
F2() is set
F3() is set
F4(0,F1(),F2(),F3()) is set
F4(1,F2(),F3(),F4(0,F1(),F2(),F3())) is set
F4(2,F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))) is set
[F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())),F4(2,F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())))] is V1() triple quadruple set
[F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))] is V1() triple set
[F3(),F4(0,F1(),F2(),F3())] is V1() set
{F3(),F4(0,F1(),F2(),F3())} is set
{F3()} is set
{{F3(),F4(0,F1(),F2(),F3())},{F3()}} is set
[[F3(),F4(0,F1(),F2(),F3())],F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))] is V1() set
{[F3(),F4(0,F1(),F2(),F3())],F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))} is set
{[F3(),F4(0,F1(),F2(),F3())]} is set
{{[F3(),F4(0,F1(),F2(),F3())],F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))},{[F3(),F4(0,F1(),F2(),F3())]}} is set
[[F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))],F4(2,F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())))] is V1() set
{[F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))],F4(2,F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())))} is set
{[F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))]} is set
{{[F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))],F4(2,F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3())))},{[F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))]}} is set

proj1 Y is set
Y . 0 is set
[F2(),F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))] is V1() triple quadruple set
[F2(),F3(),F4(0,F1(),F2(),F3())] is V1() triple set
[F2(),F3()] is V1() set
{F2(),F3()} is set
{F2()} is set
{{F2(),F3()},{F2()}} is set
[[F2(),F3()],F4(0,F1(),F2(),F3())] is V1() set
{[F2(),F3()],F4(0,F1(),F2(),F3())} is set
{[F2(),F3()]} is set
{{[F2(),F3()],F4(0,F1(),F2(),F3())},{[F2(),F3()]}} is set
[[F2(),F3(),F4(0,F1(),F2(),F3())],F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))] is V1() set
{[F2(),F3(),F4(0,F1(),F2(),F3())],F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))} is set
{[F2(),F3(),F4(0,F1(),F2(),F3())]} is set
{{[F2(),F3(),F4(0,F1(),F2(),F3())],F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))},{[F2(),F3(),F4(0,F1(),F2(),F3())]}} is set
[F1(),F2(),F3(),F4(0,F1(),F2(),F3())] is V1() triple quadruple set
[F1(),F2(),F3()] is V1() triple set
[F1(),F2()] is V1() set
{F1(),F2()} is set
{F1()} is set
{{F1(),F2()},{F1()}} is set
[[F1(),F2()],F3()] is V1() set
{[F1(),F2()],F3()} is set
{[F1(),F2()]} is set
{{[F1(),F2()],F3()},{[F1(),F2()]}} is set
[[F1(),F2(),F3()],F4(0,F1(),F2(),F3())] is V1() set
{[F1(),F2(),F3()],F4(0,F1(),F2(),F3())} is set
{[F1(),F2(),F3()]} is set
{{[F1(),F2(),F3()],F4(0,F1(),F2(),F3())},{[F1(),F2(),F3()]}} 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

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
F4(((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),F4(((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)],F4(((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)],F4(((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)],F4(((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

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
F4(((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),F4(((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)],F4(((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)],F4(((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)],F4(((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
H1(0 + 2,Z . (0 + 2)) `1_4 is set
[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2),F4(((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),F4(((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),F4(((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))