:: FINSEQ_1 semantic presentation

REAL is non empty non trivial non finite set

bool REAL is non empty non trivial non finite set

bool omega is non empty non trivial non finite set
RAT is non empty non trivial non finite set

INT is non empty non trivial non finite set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

(D) is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set
bool NAT is non empty non trivial non finite set
x is set

(f) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set
f is set

(1) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V39() 1 -element set

(2) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V39() set
D is set

D is set

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

((D + 1)) is non empty Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D + 1 ) } is set

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

(f) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
x is set

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

(f) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

(f) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
(f) /\ (D) is Element of bool NAT

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

(f) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
(D) /\ (f) is Element of bool NAT

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

{(D + 1)} is non empty trivial finite V39() 1 -element set
(D) \/ {(D + 1)} is non empty set
((D + 1)) is non empty Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D + 1 ) } is set

f is set
f is set

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

((D + 1)) is non empty Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D + 1 ) } is set
{(D + 1)} is non empty trivial finite V39() 1 -element set
((D + 1)) \ {(D + 1)} is Element of bool NAT
(D) \/ {(D + 1)} is non empty set
(D) /\ {(D + 1)} is finite Element of bool NAT
the Element of (D) /\ {(D + 1)} is Element of (D) /\ {(D + 1)}

dom D is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

(D) is Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : not D <= b1 } is set
f is set

dom f is set
rng f is set
x is set
nx is set
f . nx is set

x is set

f . ny is set

dom D is set

(f) is finite Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
rng D is set
[:(dom D),(rng D):] is Relation-like set

(D) is finite Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

(f) is finite Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

((f + 1)) is non empty finite Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f + 1 ) } is set

{f} is non empty trivial finite V39() 1 -element set
f \/ {f} is non empty finite set
{(f + 1)} is non empty trivial finite V39() 1 -element set
(f) \/ {(f + 1)} is non empty finite set
x is set
x is set

(D) is finite Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

(D) is finite Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

dom D is finite set

(f) is finite f -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

(x) is finite x -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= x ) } is set

dom nx is set
rng nx is set
ny is set
nx . ny is set
k is set
nx . k is set
D . ny is set
[ny,(D . ny)] is set
{ny,(D . ny)} is non empty finite set
{ny} is non empty trivial finite 1 -element set
{{ny,(D . ny)},{ny}} is non empty finite V39() set
D . k is set
[k,(D . k)] is set
{k,(D . k)} is non empty finite set
{k} is non empty trivial finite 1 -element set
{{k,(D . k)},{k}} is non empty finite V39() set
ny is set
k is set
nx . k is set
D . k is set
[k,(D . k)] is set
{k,(D . k)} is non empty finite set
{k} is non empty trivial finite 1 -element set
{{k,(D . k)},{k}} is non empty finite V39() set
ny is set
k is set
[ny,k] is set
{ny,k} is non empty finite set
{ny} is non empty trivial finite 1 -element set
{{ny,k},{ny}} is non empty finite V39() set
D . ny is set
nx . ny is set

dom D is finite set

((D)) is finite (D) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) ) } is set

dom D is set

(f) is finite f -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

dom x is set

ny is set
k is set
[ny,k] is set
{ny,k} is non empty finite set
{ny} is non empty trivial finite 1 -element set
{{ny,k},{ny}} is non empty finite V39() set
D . ny is set
nx . ny is set
[ny,(nx . ny)] is set
{ny,(nx . ny)} is non empty finite set
{{ny,(nx . ny)},{ny}} is non empty finite V39() set

(F1()) is finite F1() -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= F1() ) } is set
D is set

dom D is set

(f) is finite Element of bool NAT

f . x is set

(F1()) is finite F1() -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= F1() ) } is set

dom D is set

(f) is finite Element of bool NAT

f . x is set
F2(x) is set
D is set

(f) is finite Element of bool NAT
x is set
nx is set
[x,nx] is set
{x,nx} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,nx},{x}} is non empty finite V39() set

f . ny is set
[ny,(f . ny)] is set
{ny,(f . ny)} is non empty finite set
{ny} is non empty trivial finite V39() 1 -element set
{{ny,(f . ny)},{ny}} is non empty finite V39() set

(D) is finite Element of bool NAT

(f) is finite Element of bool NAT
x is set
D . x is set
f . x is set

(D) is finite Element of bool NAT
((D)) is finite (D) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) ) } is set
(f) is finite Element of bool NAT
((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set
x is set

D . x is set
f . x is set

(D) is finite D -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

dom (f | (D)) is finite set
(f) is finite Element of bool NAT
(f) /\ (D) is finite Element of bool NAT

((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set
((f)) /\ (D) is finite Element of bool NAT

dom D is set

rng f is finite set

dom (f * D) is finite set
(f) is finite Element of bool NAT

((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set

(D) is finite D -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set

(x) is finite Element of bool NAT
((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set
(f) is finite Element of bool NAT
D is set
D is set
f is Relation-like Function-like finite () (D)
rng f is finite set
D is set

bool [:NAT,D:] is non empty set
f is Relation-like D -valued Function-like finite () (D)
(f) is finite Element of bool NAT
rng f is finite set

D is set

bool [:NAT,D:] is non empty set
D is set

bool [:NAT,D:] is non empty set
f is Relation-like D -valued Function-like finite () (D)

(D) is finite D -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= D ) } is set
f is set

bool [:NAT,f:] is non empty set
rng (x | (D)) is finite set
rng x is finite set

f is non empty set
the Element of f is Element of f

(x) is finite x -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= x ) } is set
(x) --> the Element of f is Relation-like (x) -defined f -valued Function-like V25((x),f) finite Element of bool [:(x),f:]
[:(x),f:] is Relation-like set
bool [:(x),f:] is non empty set
dom ((x) --> the Element of f) is finite set

rng k is finite set
{ the Element of f} is non empty trivial finite 1 -element set

D is set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

D is set
D is set
(D) is Relation-like NAT -defined D -valued Function-like finite () (D)
D is set

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) + (f) ) } is set
(D) is finite Element of bool NAT
(f) is finite Element of bool NAT

x is set

nx - (D) is ext-real V33() complex V43() set
f . (nx - (D)) is set

D . k is set

k - (D) is ext-real V33() complex V43() set
f . (k - (D)) is set
D . nx is set

D . k is set

j - (D) is ext-real V33() complex V43() set
f . (j - (D)) is set
ny is set
k is set

dom x is set

x . nx is set
D . nx is set
((D)) is finite (D) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) ) } is set

x . ((D) + nx) is set
f . nx is set
((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set

x . ((D) + ny) is set

(ny + (D)) - (D) is ext-real V33() complex V43() set
f . ((ny + (D)) - (D)) is set

(nx) is finite Element of bool NAT

nx . ny is set
D . ny is set

nx . ((D) + k) is set
f . k is set

(x) is finite Element of bool NAT

(nx) is finite Element of bool NAT
ny is set
x . ny is set
nx . ny is set

((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set
nx . ((D) + (1 + x8)) is set
f . (1 + x8) is set
((D)) is finite (D) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) ) } is set
x . k is set
D . k is set

(D) is finite Element of bool NAT

(D,f) is Relation-like Function-like finite () set
(D,f) | (D) is Relation-like Function-like finite set
((D,f)) is finite Element of bool NAT

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) + (f) ) } is set
((D)) is finite (D) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) ) } is set
((D,f)) /\ ((D)) is finite Element of bool NAT
x is set
D . x is set
(D,f) . x is set

(D,f) is Relation-like Function-like finite () set

((D,f)) is finite Element of bool NAT
(((D) + (f))) is finite (D) + (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) + (f) ) } is set

(D,f) is Relation-like Function-like finite () set

(D,f) . x is set
x - (D) is ext-real V33() complex V43() set
f . (x - (D)) is set

((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set
(f) is finite Element of bool NAT

(D,f) is Relation-like Function-like finite () set

(D,f) . x is set
x - (D) is ext-real V33() complex V43() set
f . (x - (D)) is set

(D) is finite Element of bool NAT

(D,f) is Relation-like Function-like finite () set
((D,f)) is finite Element of bool NAT
(f) is finite Element of bool NAT

(((D,f))) is finite ((D,f)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= ((D,f)) ) } is set

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) + (f) ) } is set

((D)) is finite (D) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) ) } is set

((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set

(D) is finite Element of bool NAT

(D,f) is Relation-like Function-like finite () set
((D,f)) is finite Element of bool NAT

((D)) is finite (D) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) ) } is set
(((D) + (f))) is finite (D) + (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) + (f) ) } is set
D is set

(f) is finite Element of bool NAT

(x,f) is Relation-like Function-like finite () set
((x,f)) is finite Element of bool NAT

((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set

(((x) + (f))) is finite (x) + (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (x) + (f) ) } is set

(f) is finite Element of bool NAT

(x,f) is Relation-like Function-like finite () set
((x,f)) is finite Element of bool NAT

rng D is finite set

(D,f) is Relation-like Function-like finite () set
rng (D,f) is finite set
x is set
(D) is finite Element of bool NAT
nx is set
D . nx is set
((D,f)) is finite Element of bool NAT

(D,f) . ny is set
D . ny is set

rng D is finite set

(f,D) is Relation-like Function-like finite () set
rng (f,D) is finite set
x is set
(D) is finite Element of bool NAT
nx is set
D . nx is set

((f,D)) is finite Element of bool NAT
(f,D) . ((f) + ny) is set
D . ny is set

rng D is finite set

(D,f) is Relation-like Function-like finite () set
rng (D,f) is finite set
rng f is finite set
(rng D) \/ (rng f) is finite set
x is set
((D,f)) is finite Element of bool NAT
nx is set
(D,f) . nx is set

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) + (f) ) } is set

ny - (D) is ext-real V33() complex V43() set
f . (ny - (D)) is set

((f)) is finite (f) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (f) ) } is set
(f) is finite Element of bool NAT
((D)) is finite (D) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) ) } is set
(D) is finite Element of bool NAT
D . ny is set

(D,f) is Relation-like Function-like finite () set

((D,f),x) is Relation-like Function-like finite () set
(f,x) is Relation-like Function-like finite () set
(D,(f,x)) is Relation-like Function-like finite () set
(((D,f),x)) is finite Element of bool NAT

((((D,f)) + (x))) is finite ((D,f)) + (x) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= ((D,f)) + (x) ) } is set

((((D) + (f)) + (x))) is finite ((D) + (f)) + (x) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= ((D) + (f)) + (x) ) } is set

(((D) + ((f) + (x)))) is finite (D) + ((f) + (x)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) + ((f) + (x)) ) } is set

(((D) + ((f,x)))) is finite (D) + ((f,x)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) + ((f,x)) ) } is set
(D) is finite Element of bool NAT

((D,f),x) . nx is set
D . nx is set
((D,f)) is finite Element of bool NAT
(D,f) . nx is set
((f,x)) is finite Element of bool NAT

((D,f),x) . ((D) + nx) is set
(f,x) . nx is set
(f) is finite Element of bool NAT
((D,f)) is finite Element of bool NAT
(D,f) . ((D) + nx) is set
f . nx is set
(x) is finite Element of bool NAT

((D,f),x) . (((D) + (f)) + ny) is set

((D,f),x) . (((D,f)) + ny) is set
x . ny is set

(D,f) is Relation-like Function-like finite () set
(f,D) is Relation-like Function-like finite () set

(x,f) is Relation-like Function-like finite () set
(f,x) is Relation-like Function-like finite () set

(D) is finite Element of bool NAT
((x)) is finite (x) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (x) ) } is set
(x) is finite Element of bool NAT

D . nx is set
x . nx is set
(x,f) . nx is set

D . nx is set
x . nx is set

(f,x) . ((f) + nx) is set

((D,{})) is finite Element of bool NAT

(((D,{}))) is finite ((D,{})) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= ((D,{})) ) } is set

(((D) + ({}))) is finite (D) + ({}) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (D) + ({}) ) } is set
(D) is finite Element of bool NAT

D . f is set
(D,{}) . f is set
(({},D)) is finite Element of bool NAT

((({},D))) is finite (({},D)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= (({},D)) ) } is set

((({}) + (D))) is finite ({}) + (D) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( 1 <= b1 & b1 <= ({}) + (D) ) } is set

D . f is set
({},D) . f is set

({},D) . (({}) + f) is set

(D,f) is Relation-like Function-like finite () set

D is set

(f,x) is Relation-like Function-like finite () set
rng (f,x) is finite set
rng f is finite set
rng x is finite set
(rng f) \/ (rng x) is finite set
D is set
f is set
[D,f] is set
{D,f} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,f},{D}} is non empty finite V39() set
x is set
nx is set
[x,nx] is set
{x,nx} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,nx},{x}} is non empty finite V39() set

D is set
(D) is set
[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

dom f is set
f . 1 is set
[1,(f . 1)] is set
{1,(f . 1)} is non empty finite set
{{1,(f . 1)},{1}} is non empty finite V39() set

nx is set
ny is set
[nx,ny] is set
{nx,ny} is non empty finite set
{nx} is non empty trivial finite 1 -element set
{{nx,ny},{nx}} is non empty finite V39() set
rng f is set
{(f . 1)} is non empty trivial finite 1 -element set
D is set

[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

D is set

[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

dom (D) is set

(D,f) is Relation-like Function-like finite () set
x is set
rng (D,f) is finite set
rng D is finite set
rng f is finite set
(rng D) \/ (rng f) is finite set
D is set

[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

f is set

[1,f] is set
{1,f} is non empty finite set
{{1,f},{1}} is non empty finite V39() set

((D),(f)) is Relation-like Function-like finite () set
x is set

[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V39() set

(((D),(f)),(x)) is Relation-like Function-like finite () set
D is set
f is set
(D,f) is set

[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

[1,f] is set
{1,f} is non empty finite set
{{1,f},{1}} is non empty finite V39() set

((D),(f)) is Relation-like Function-like finite () set
x is set
(D,f,x) is set

[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V39() set

(((D),(f)),(x)) is Relation-like Function-like finite () set
D is set
f is set
(D,f) is Relation-like Function-like set

[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

[1,f] is set
{1,f} is non empty finite set
{{1,f},{1}} is non empty finite V39() set

((D),(f)) is Relation-like Function-like finite () set
x is set
(D,f,x) is Relation-like Function-like set

[1,x] is set
{1,x} is non empty finite set
{{1,x},{1}} is non empty finite V39() set

(((D),(f)),(x)) is Relation-like Function-like finite () set
D is set

[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

D is set

[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

{D} is non empty trivial finite 1 -element set

(f) is finite Element of bool NAT
rng f is finite set
f . 1 is set
{(f . 1)} is non empty trivial finite 1 -element set
f . 1 is set
D is set

[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set

{D} is non empty trivial finite 1 -element set

rng f is finite set
(f) is finite Element of bool NAT
D is set

[1,D] is set
{1,D} is non empty finite set
{{1,D},{1}} is non empty finite V39() set
{[1,D]} is