:: FINSEQ_1 semantic presentation

REAL is non empty non trivial non finite set

NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty non trivial non finite set

omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal set

bool omega is non empty non trivial non finite set

RAT is non empty non trivial non finite set

{} is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued set

the Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued set is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued set

1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

INT is non empty non trivial non finite set

0 is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued Element of NAT

dom {} is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued set

rng {} is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

{ b

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is set

{ b

bool NAT is non empty non trivial non finite set

x is set

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(f) is Element of bool NAT

{ b

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

D is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued set

(D) is Element of bool NAT

{ b

f is set

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(1) is Element of bool NAT

{ b

{1} is non empty trivial finite V39() 1 -element set

2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

(2) is Element of bool NAT

{ b

{1,2} is non empty finite V39() set

D is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

D is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is Element of bool NAT

{ b

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() set

(D) is Element of bool NAT

{ b

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

D + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

((D + 1)) is non empty Element of bool NAT

{ b

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is Element of bool NAT

{ b

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(f) is Element of bool NAT

{ b

x is set

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is Element of bool NAT

{ b

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(f) is Element of bool NAT

{ b

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is Element of bool NAT

{ b

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(f) is Element of bool NAT

{ b

(f) /\ (D) is Element of bool NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is Element of bool NAT

{ b

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(f) is Element of bool NAT

{ b

(D) /\ (f) is Element of bool NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is Element of bool NAT

{ b

D + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

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

{ b

D + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

f is set

f is set

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is Element of bool NAT

{ b

D + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

((D + 1)) is non empty Element of bool NAT

{ b

{(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)}

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

D is Relation-like set

dom D is set

(0) is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued Element of bool NAT

{ b

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is Element of bool NAT

{ b

{ b

f is set

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

f is Relation-like Function-like set

dom f is set

rng f is set

x is set

nx is set

f . nx is set

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

ny + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

x is set

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

1 + ny is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

f . ny is set

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

k + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

D is Relation-like Function-like set

dom D is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(f) is finite Element of bool NAT

{ b

rng D is set

[:(dom D),(rng D):] is Relation-like set

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is finite Element of bool NAT

{ b

(0) is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued () Element of bool NAT

{ b

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(f) is finite Element of bool NAT

{ b

f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

((f + 1)) is non empty finite Element of bool NAT

{ b

succ f is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of omega

{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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is finite Element of bool NAT

{ b

card (D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of omega

card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of omega

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is finite Element of bool NAT

{ b

card (D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of omega

card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of omega

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

card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of omega

dom D is finite set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) is finite f -element Element of bool NAT

{ b

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(x) is finite x -element Element of bool NAT

{ b

nx is Relation-like Function-like 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

card D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of omega

card (dom D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

card x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of omega

card f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of omega

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

dom D is finite set

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((D)) is finite (D) -element Element of bool NAT

{ b

D is Relation-like Function-like set

dom D is set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(f) is finite f -element Element of bool NAT

{ b

x is Relation-like Function-like set

dom x is set

nx is Relation-like Function-like finite () 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

F

(F

{ b

D is set

D is Relation-like Function-like set

dom D is set

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

(f) is finite Element of bool NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

f . x is set

F

(F

{ b

D is Relation-like Function-like set

dom D is set

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

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) is finite Element of bool NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

f . x is set

F

D is set

f is Relation-like Function-like finite () 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

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 Relation-like Function-like finite () set

(D) is finite Element of bool NAT

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

(f) is finite Element of bool NAT

x is set

D . x is set

f . x is set

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

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) is finite Element of bool NAT

((D)) is finite (D) -element Element of bool NAT

{ b

(f) is finite Element of bool NAT

((f)) is finite (f) -element Element of bool NAT

{ b

x is set

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

D . x is set

f . x is set

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is finite D -element Element of bool NAT

{ b

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

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

dom (f | (D)) is finite set

(f) is finite Element of bool NAT

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

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((f)) is finite (f) -element Element of bool NAT

{ b

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

D is Relation-like Function-like set

dom D is set

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

rng f is finite set

f * D is Relation-like Function-like finite set

dom (f * D) is finite set

(f) is finite Element of bool NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((f)) is finite (f) -element Element of bool NAT

{ b

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is finite D -element Element of bool NAT

{ b

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

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

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

(x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(x) is finite Element of bool NAT

((f)) is finite (f) -element Element of bool NAT

{ b

(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

[:NAT,D:] is Relation-like 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 Relation-like set

D is set

[:NAT,D:] is Relation-like set

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

D is set

[:NAT,D:] is Relation-like set

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

f is Relation-like D -valued Function-like finite () (D)

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) is finite D -element Element of bool NAT

{ b

f is set

x is Relation-like NAT -defined f -valued Function-like finite () (f)

x | (D) is Relation-like NAT -defined (D) -defined NAT -defined f -valued Function-like finite Element of bool [:NAT,f:]

[:NAT,f:] is Relation-like set

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

rng (x | (D)) is finite set

rng x is finite set

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

f is non empty set

the Element of f is Element of f

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(x) is finite x -element Element of bool NAT

{ b

(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

k is Relation-like Function-like finite () set

rng k is finite set

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

j is Relation-like NAT -defined f -valued Function-like finite () (f)

(j) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of 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 Relation-like Function-like constant non empty trivial finite 1 -element set

D is set

D is set

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

D is set

(D) is Relation-like non-empty empty-yielding NAT -defined D -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued () (D)

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

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT

{ b

(D) is finite Element of bool NAT

(f) is finite Element of bool NAT

(D) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

x is set

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

f . (nx - (D)) is set

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

D . k is set

nx + ((D) + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

nx + (D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(nx + (D)) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

(nx + (D)) + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

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

f . (k - (D)) is set

D . nx is set

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

D . k is set

j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

j - (D) is ext-real V33() complex V43() set

f . (j - (D)) is set

ny is set

k is set

x is Relation-like Function-like set

dom x is set

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

x . nx is set

D . nx is set

((D)) is finite (D) -element Element of bool NAT

{ b

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) + nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

x . ((D) + nx) is set

f . nx is set

((f)) is finite (f) -element Element of bool NAT

{ b

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((D) + ny) + (D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

x . ((D) + ny) is set

ny + (D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

f . ((ny + (D)) - (D)) is set

nx is Relation-like Function-like finite () set

(nx) is finite Element of bool NAT

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

nx . ny is set

D . ny is set

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

nx . ((D) + k) is set

f . k is set

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

(x) is finite Element of bool NAT

nx is Relation-like Function-like finite () set

(nx) is finite Element of bool NAT

ny is set

x . ny is set

nx . ny is set

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

((D) + 1) + j is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

x8 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

1 + x8 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

(D) + (1 + x8) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

1 + 0 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

((f)) is finite (f) -element Element of bool NAT

{ b

nx . ((D) + (1 + x8)) is set

f . (1 + x8) is set

((D)) is finite (D) -element Element of bool NAT

{ b

x . k is set

D . k is set

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

(D) is finite Element of bool NAT

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

(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) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT

{ b

((D)) is finite (D) -element Element of bool NAT

{ b

((D,f)) /\ ((D)) is finite Element of bool NAT

x is set

D . x is set

(D,f) . x is set

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

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

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

((D,f)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((D,f)) is finite Element of bool NAT

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT

{ b

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

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

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

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D,f) . x is set

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

f . (x - (D)) is set

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

((D) + 1) + nx is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

1 + ny is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

(D) + (1 + ny) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

((f)) is finite (f) -element Element of bool NAT

{ b

(f) is finite Element of bool NAT

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

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

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

((D,f)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D,f) . x is set

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

f . (x - (D)) is set

(D) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

(D) is finite Element of bool NAT

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

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

((D,f)) is finite Element of bool NAT

(f) is finite Element of bool NAT

x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

((D,f)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(((D,f))) is finite ((D,f)) -element Element of bool NAT

{ b

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT

{ b

(D) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

((D)) is finite (D) -element Element of bool NAT

{ b

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

((D) + 1) + nx is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

1 + ny is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

(D) + (1 + ny) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

((f)) is finite (f) -element Element of bool NAT

{ b

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) + nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) + ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

(D) is finite Element of bool NAT

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

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

((D,f)) is finite Element of bool NAT

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((D)) is finite (D) -element Element of bool NAT

{ b

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT

{ b

D is set

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

(f) is finite Element of bool NAT

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

(x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

((x,f)) is finite Element of bool NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((f)) is finite (f) -element Element of bool NAT

{ b

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(x) + nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(x) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(((x) + (f))) is finite (x) + (f) -element Element of bool NAT

{ b

D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

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

(f) is finite Element of bool NAT

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

(x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(x) + D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

((x,f)) is finite Element of bool NAT

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(x) + nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

rng D is finite set

f is Relation-like Function-like 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

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D,f) . ny is set

D . ny is set

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

rng D is finite set

f is Relation-like Function-like 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) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) + ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((f,D)) is finite Element of bool NAT

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

D . ny is set

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

rng D is finite set

f is Relation-like Function-like 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) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(((D) + (f))) is finite (D) + (f) -element Element of bool NAT

{ b

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

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

f . (ny - (D)) is set

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

((D) + 1) + k is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

1 + j is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

(D) + (1 + j) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

1 + 0 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT

((f)) is finite (f) -element Element of bool NAT

{ b

(f) is finite Element of bool NAT

((D)) is finite (D) -element Element of bool NAT

{ b

(D) is finite Element of bool NAT

D . ny is set

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

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

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

x 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)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((D,f)) + (x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((((D,f)) + (x))) is finite ((D,f)) + (x) -element Element of bool NAT

{ b

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((D) + (f)) + (x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((((D) + (f)) + (x))) is finite ((D) + (f)) + (x) -element Element of bool NAT

{ b

(f) + (x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + ((f) + (x)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(((D) + ((f) + (x)))) is finite (D) + ((f) + (x)) -element Element of bool NAT

{ b

((f,x)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + ((f,x)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(((D) + ((f,x)))) is finite (D) + ((f,x)) -element Element of bool NAT

{ b

(D) is finite Element of bool NAT

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

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

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(D) + nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of 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

ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

(f) + ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((D) + (f)) + ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

((D,f)) + ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

x . ny is set

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

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

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

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

x 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((x,f)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(x) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) is finite Element of bool NAT

((x)) is finite (x) -element Element of bool NAT

{ b

(x) is finite Element of bool NAT

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

D . nx is set

x . nx is set

(x,f) . nx is set

(f) + (D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((f,x)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) + (x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

D . nx is set

x . nx is set

(f) + nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

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

(D,{}) is Relation-like Function-like finite () set

({},D) is Relation-like Function-like finite () set

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

((D,{})) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

{ b

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

({}) is Relation-like non-empty empty-yielding RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V33() complex finite finite-yielding V39() cardinal {} -element V43() complex-valued ext-real-valued real-valued natural-valued () Element of NAT

(D) + ({}) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(((D) + ({}))) is finite (D) + ({}) -element Element of bool NAT

{ b

(D) is finite Element of bool NAT

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

D . f is set

(D,{}) . f is set

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

(({},D)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

{ b

({}) + (D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

((({}) + (D))) is finite ({}) + (D) -element Element of bool NAT

{ b

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set

D . f is set

({},D) . f is set

({}) + f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

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

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

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

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

((D,f)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

D is set

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

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

(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

{[x,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element 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

{[1,D]} is Relation-like Function-like constant non empty trivial finite 1 -element set

f is Relation-like Function-like 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

{[1,(f . 1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set

x is Relation-like Function-like 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

(D) 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,D]} is Relation-like Function-like constant non empty trivial finite 1 -element set

D is set

(D) 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,D]} is Relation-like Function-like constant non empty trivial finite 1 -element set

dom (D) is set

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

f is Relation-like Function-like finite () 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

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

[1,D] is set

{1,D} is non empty finite set

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

{[1,D]} is Relation-like Function-like constant non empty trivial finite 1 -element set

f is set

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

[1,f] is set

{1,f} is non empty finite set

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

{[1,f]} is Relation-like Function-like constant non empty trivial finite 1 -element set

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

x is set

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

[1,x] is set

{1,x} is non empty finite set

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

{[1,x]} is Relation-like Function-like constant non empty trivial finite 1 -element set

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

D is set

f is set

(D,f) is set

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

[1,D] is set

{1,D} is non empty finite set

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

{[1,D]} is Relation-like Function-like constant non empty trivial finite 1 -element set

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

[1,f] is set

{1,f} is non empty finite set

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

{[1,f]} is Relation-like Function-like constant non empty trivial finite 1 -element set

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

x is set

(D,f,x) is set

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

[1,x] is set

{1,x} is non empty finite set

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

{[1,x]} is Relation-like Function-like constant non empty trivial finite 1 -element 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

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

[1,D] is set

{1,D} is non empty finite set

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

{[1,D]} is Relation-like Function-like constant non empty trivial finite 1 -element set

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

[1,f] is set

{1,f} is non empty finite set

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

{[1,f]} is Relation-like Function-like constant non empty trivial finite 1 -element set

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

x is set

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

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

[1,x] is set

{1,x} is non empty finite set

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

{[1,x]} is Relation-like Function-like constant non empty trivial finite 1 -element set

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

D is set

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

[1,D] is set

{1,D} is non empty finite set

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

{[1,D]} is Relation-like Function-like constant non empty trivial finite 1 -element set

D is set

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

[1,D] is set

{1,D} is non empty finite set

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

{[1,D]} is Relation-like Function-like constant non empty trivial finite 1 -element set

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

f is Relation-like Function-like finite () 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

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

[1,D] is set

{1,D} is non empty finite set

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

{[1,D]} is Relation-like Function-like constant non empty trivial finite 1 -element set

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

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

(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT

rng f is finite set

(f) is finite Element of bool NAT

D is set

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

[1,D] is set

{1,D} is non empty finite set

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

{[1,D]} is