:: 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

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

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

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

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

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

F

F

(X +* f) . f3 is set

X . f3 is set

f . f3 is set

Z . f3 is set

F

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

F

F

F

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

F

[:NAT,F

bool [:NAT,F

[:NAT,F

bool [:NAT,F

F

F

[:F

x is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

y is Element of [:F

y `1 is set

y `2 is set

y `1 is Element of F

y `2 is Element of F

X is Element of F

Y is Element of F

[X,Y] is V1() Element of [:F

{X,Y} is set

{X} is set

{{X,Y},{X}} is set

[X,Y] `1 is set

[X,Y] `2 is set

[:NAT,[:F

bool [:NAT,[:F

[F

{F

{F

{{F

x is Relation-like NAT -defined [:F

x . 0 is Element of [:F

pr1 x is Relation-like NAT -defined F

(pr1 x) . 0 is Element of F

pr2 x is Relation-like NAT -defined F

(pr2 x) . 0 is Element of F

[F

[F

y is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

(pr1 x) . y is Element of F

(pr2 x) . y is Element of F

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

(pr2 x) . (y + 1) is Element of F

x . (y + 1) is Element of [:F

(x . (y + 1)) `1 is Element of F

(x . (y + 1)) `2 is Element of F

x . y is Element of [:F

(x . y) `1 is Element of F

(x . y) `2 is Element of F

F

F

F

F

[F

[F

{F

{F

{{F

[[F

{[F

{[F

{{[F

X is Relation-like Function-like set

proj1 X is set

X . 0 is set

[F

[F

{F

{F

{{F

[[F

{[F

{[F

{{[F

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

[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2),F

[((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

{[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)],F

{[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)]} is set

{{[((Y . (f + 1)) `2_3),((Y . (f + 1)) `2)],F

(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

[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F

[((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

{[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)],F

{[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)]} is set

{{[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2)],F

H

[((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F

([((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F

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

(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) + 1) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

F

[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F

[((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

{[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2)],F

{[((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

H

[((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F

([((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F

H

([((Y . ((f + 1) + 1)) `2_3),((Y . ((f + 1) + 1)) `2),F

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

[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2),F

[((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

{[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)],F

{[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)]} is set

{{[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2)],F

H

[((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2),F

([((Y . (1 + 1)) `2_3),((Y . (1 + 1)) `2),F

(Y . 0) `2 is set

F

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

[((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2),F

[((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

{[((Y . ((f -' 1) + 1)) `2_3),((Y . ((f -' 1) + 1)) `2)],F

{[((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

H

Z . (0 + 2) is set

(Y . (0 + 2)) `1_3 is set

((Y . (0 + 2)) `1) `1 is set

H

([((Y . (0 + 1)) `2_3),((Y . (0 + 1)) `2),F

(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

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

[:NAT,F

bool [:NAT,F

F

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 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

F

proj1 F

F

F

F

F

F

proj1 F

F

F

x is set

F

F

x is ext-real non negative V24() V25() V26() V30() V31() V32() V33() set

F

F

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

F

(x -' 2) + 1 is non empty ext-real positive non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

F

F

F

F

F

F

(x -' 2) + 0 is ext-real non negative V24() V25() V26() V30() V31() V32() V33() Element of NAT

F

[:NAT,F

bool [:NAT,F

F

F

F

F

F

F

F

F

proj1 F

proj1 F

F

F

F

F

F

F

[F

[F

[F

{F

{F

{{F

[[F

{[F

{[F

{{[F

[[F

{[F

{[F

{{[F

Y is Relation-like Function-like set

proj1 Y is set

Y . 0 is set

[F

[F

[F

{F

{F

{{F

[[F

{[F

{[F

{{[F

[[F

{[F

{[F

{{[F

[F

[F

[F

{F

{F

{{F

[[F

{[F

{[F

{{[F

[[F

{[F

{[F

{{[F

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

[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2),F

[((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

{[((Z . (f + 2)) `2_4),((Z . (f + 2)) `2_3),((Z . (f + 2)) `2)],F

{[((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

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

[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2),F

[((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

{[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2)],F

{[((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

H

[((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2),F

([((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2),F

(([((Z . (0 + 2)) `2_4),((Z . (0 + 2)) `2_3),((Z . (0 + 2)) `2),F

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))