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
{ 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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
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
{ 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 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
{ 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
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
{ 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 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
{ 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
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
{ 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 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
{ 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 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
{ 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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
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
{ 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 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
{ 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 + 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
{ 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 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
{ 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)}
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
{ 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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
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
{ 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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
(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
{ 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 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
{ 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
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
{ 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
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
{ 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
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
{ 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 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
{ 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
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
{ 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 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
{ 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 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
F1() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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
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
F1() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() 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 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
F2(x) is set
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
{ 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
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
{ 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 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
{ 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
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
{ 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 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
{ 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 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
{ 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
[: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
{ 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
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
{ 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
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
{ 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
(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
{ 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
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
{ 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
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
{ 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 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
{ 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 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
{ 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 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
{ 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 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
{ 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
(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
{ 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) + 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
{ 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
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
{ 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 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
{ 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 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
{ 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 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
{ 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
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
{ 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 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
{ 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 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
{ 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 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
{ 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
(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
{ 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
((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
{ 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
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
{ 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
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
{ 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 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
{ 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
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
{ 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 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
{ 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 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 Relation-like Function-like constant 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
f . 1 is 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 Relation-like Function-like constant non empty trivial finite 1 -element set
f is Relation-like Function-like finite () set
((D),f) is Relation-like Function-like finite () set
((D),f) . 1 is set
((D)) is finite Element of bool NAT
(D) . 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
f is Relation-like Function-like finite () set
(f,(D)) 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) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(f,(D)) . ((f) + 1) is set
((D)) is finite Element of bool NAT
(D) . 1 is set
D is set
f is set
x is set
(D,f,x) is Relation-like Function-like finite () 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 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
(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
nx is set
ny is set
k is set
(nx,ny,k) is Relation-like Function-like finite () set
(nx) is Relation-like Function-like finite () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(ny) is Relation-like Function-like finite () set
[1,ny] is set
{1,ny} is non empty finite set
{{1,ny},{1}} is non empty finite V39() set
{[1,ny]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((nx),(ny)) is Relation-like Function-like finite () set
(k) is Relation-like Function-like finite () set
[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V39() set
{[1,k]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((nx),(ny)),(k)) is Relation-like Function-like finite () set
(nx,ny) is Relation-like Function-like finite () set
((nx,ny),(k)) is Relation-like Function-like finite () set
D is set
f is set
(D,f) is Relation-like Function-like finite () 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 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 . 1 is set
x . 2 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
1 + ((f)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive 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 finite Element of bool NAT
(D) . 1 is set
((f)) is finite Element of bool NAT
((D),(f)) . (1 + 1) 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
((D),(f)) . (((D)) + 1) is set
(f) . 1 is set
(x) is finite Element of bool 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
((1 + 1)) is non empty finite 1 + 1 -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 <= 1 + 1 ) } is 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
((((D)) + 1)) is non empty finite ((D)) + 1 -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)) + 1 ) } 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 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
{ 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
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
((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
((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
1 + nx is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
x . (1 + nx) is set
x . (1 + 1) is set
(f) . 1 is set
3 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
f is set
x is set
(D,f,x) is Relation-like Function-like finite () 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 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
nx is Relation-like Function-like finite () set
(nx) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
nx . 1 is set
nx . 2 is set
nx . 3 is 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() 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
2 + ((x)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
2 + 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 Element of bool NAT
(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)) . 1 is set
(D) . 1 is set
((D,f)) is finite Element of bool NAT
(D,f) . 2 is set
((x)) is finite Element of bool NAT
((D,f),(x)) is Relation-like Function-like finite () set
((D,f),(x)) . (2 + 1) is set
((D,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,f),(x)) . (((D,f)) + 1) is set
(x) . 1 is set
(nx) is finite Element of bool NAT
2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((2 + 1)) is non empty finite 2 + 1 -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 <= 2 + 1 ) } is 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,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,f)) + 1)) is non empty finite ((D,f)) + 1 -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)) + 1 ) } is set
((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
{ 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)) 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,f) . ny 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
((D,f)) + ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
nx . (((D,f)) + ny) is set
(x) . ny is set
nx . (2 + 1) 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 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
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
{ 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
D | (x) is Relation-like Function-like finite set
nx is Relation-like Function-like finite () set
D . (D) is set
((D . (D))) is Relation-like Function-like finite () set
[1,(D . (D))] is set
{1,(D . (D))} is non empty finite set
{{1,(D . (D))},{1}} is non empty finite V39() set
{[1,(D . (D))]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(nx,((D . (D)))) is Relation-like Function-like finite () set
(nx) is finite Element of bool NAT
(D) is finite Element of bool NAT
(D) /\ (x) 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)) /\ (x) is finite Element of bool NAT
((nx,((D . (D))))) is finite Element of bool NAT
((nx,((D . (D))))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(((nx,((D . (D)))))) is finite ((nx,((D . (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 <= ((nx,((D . (D))))) ) } is set
(nx) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(((D . (D)))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(nx) + (((D . (D)))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(((nx) + (((D . (D)))))) is finite (nx) + (((D . (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 <= (nx) + (((D . (D)))) ) } is set
(nx) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((nx) + 1)) is non empty finite (nx) + 1 -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 <= (nx) + 1 ) } is set
ny is set
D . ny is set
(nx,((D . (D)))) . ny is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((x + 1)) is non empty finite x + 1 -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 + 1 ) } is set
{(x + 1)} is non empty trivial finite V39() 1 -element set
(x) \/ {(x + 1)} is non empty finite set
D . k is set
nx . k is set
(nx,((D . (D)))) . k is set
(((D . (D)))) is finite Element of bool NAT
(nx,((D . (D)))) . (x + 1) is set
(nx,((D . (D)))) . ((nx) + 1) is set
((D . (D))) . 1 is set
D . (x + 1) is set
D is non empty set
f is Element of D
(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
x is set
rng (f) is finite set
(f) is Relation-like Function-like finite () set
rng (f) is finite set
{f} is non empty trivial finite 1 -element set
D is Relation-like Function-like finite () set
f is Element of bool REAL
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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
nx is Relation-like Function-like finite () set
(nx) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
ny is Relation-like Function-like finite () set
k is set
(k) is Relation-like Function-like finite () set
[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V39() set
{[1,k]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(ny,(k)) is Relation-like Function-like finite () set
(ny) 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() Element of NAT
(ny) + ((k)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(ny) + 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 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
(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 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
x is Relation-like Function-like finite () set
({},x) 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
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
((D,(f))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of 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
nx is Relation-like Function-like finite () set
(x,nx) is Relation-like Function-like finite () set
ny is Relation-like Function-like finite () set
((D,(f)),ny) is Relation-like Function-like finite () set
(x) 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 Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
x . k is set
(D,(f)) . k is set
((D,(f)),ny) . k is set
(x,{}) 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) + 1 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 Relation-like Function-like finite () set
(D,((f),ny)) is Relation-like Function-like finite () set
k is Relation-like Function-like finite () set
(x,k) is Relation-like Function-like finite () set
(k,(f)) is Relation-like Function-like finite () set
(x,(k,(f))) is Relation-like Function-like finite () set
k is Relation-like Function-like finite () set
(x,k) is Relation-like Function-like finite () set
j is Relation-like Function-like finite () set
(x,j) is Relation-like Function-like finite () 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
nx is Relation-like Function-like finite () set
(x,nx) 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
(x) 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 set
[:NAT,D:] is Relation-like set
bool [:NAT,D:] is non empty set
f is set
x is set
nx is Relation-like NAT -defined D -valued Function-like finite () (D)
f is set
x is set
nx is set
D is set
(D) is set
the Relation-like NAT -defined D -valued Function-like finite () (D) is Relation-like NAT -defined D -valued Function-like finite () (D)
D is Relation-like NAT -defined Function-like finite () set
rng D is 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 NAT -defined Function-like finite () set
rng f is finite set
(f) 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 NAT -defined 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
x is Relation-like NAT -defined Function-like finite () set
rng x is finite set
(x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x is Relation-like NAT -defined Function-like finite () set
rng x is finite set
(x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
nx is set
(nx) is Relation-like NAT -defined Function-like finite () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(x,(nx)) is Relation-like NAT -defined Function-like finite () set
rng (x,(nx)) is finite set
ny is Relation-like NAT -defined Function-like finite () set
rng ny is finite set
rng (nx) is finite set
(rng x) \/ (rng (nx)) is finite set
{nx} is non empty trivial finite 1 -element set
(rng x) \/ {nx} is non empty finite set
(ny) is finite Element of bool NAT
k is set
ny . k is set
(ny) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
((ny)) is finite (ny) -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 <= (ny) ) } is set
j is epsilon-transitive epsilon-connected ordinal natural ext-real 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() set
1 + x8 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
x9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
j + x9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(p) is finite p -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 <= p ) } is set
ny | (p) is Relation-like (p) -defined NAT -defined Function-like finite set
p17 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(p17) is finite p17 -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 <= p17 ) } is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
j + f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny . (j + f) is set
f is Relation-like NAT -defined Function-like finite () set
(f) is finite Element of bool NAT
q9 is Relation-like NAT -defined Function-like finite () set
(q9) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(q9,(nx)) is Relation-like NAT -defined Function-like finite () set
((q9,(nx))) 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
((q9,(nx))) + (f) 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() Element of NAT
(q9) + ((nx)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
((q9) + ((nx))) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
p + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(p + 1) + (f) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((q9,(nx))) + (f))) is finite ((q9,(nx))) + (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 <= ((q9,(nx))) + (f) ) } is set
(q9,f) is Relation-like NAT -defined Function-like finite () set
rng (q9,f) is finite set
(rng ny) \ {nx} is finite Element of bool (rng ny)
bool (rng ny) is non empty finite V39() set
l is set
rng q9 is finite set
rng f is finite set
(rng q9) \/ (rng f) is finite set
ny .: (p) is finite set
(q9) is finite Element of bool NAT
m is set
q9 . m is set
ny . m is set
((q9)) is finite (q9) -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 <= (q9) ) } is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
m is set
f . m is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
f . k1 is set
j + k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny . (j + k1) is set
l is set
m is set
ny . m is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
j + k2 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() Element of NAT
j + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
f . k is set
rng f is finite set
(q9) is finite Element of bool NAT
q9 . k1 is set
rng q9 is finite set
(rng q9) \/ (rng f) is finite set
(x) is finite Element of bool NAT
(x,(nx)) | (x) is Relation-like (x) -defined NAT -defined Function-like finite set
(rng (x,(nx))) \ {nx} is finite Element of bool (rng (x,(nx)))
bool (rng (x,(nx))) is non empty finite V39() set
l is set
m is set
x . m 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
(x) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(x,(nx)) . ((x) + 1) is set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(x,(nx)) . k1 is set
x . k1 is set
(((x) + 1)) is non empty finite (x) + 1 -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) + 1 ) } is set
(x) + ((nx)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(((x) + ((nx)))) is finite (x) + ((nx)) -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) + ((nx)) ) } is set
((x,(nx))) is finite Element of bool NAT
l is set
l is set
dom (q9,f) is finite set
(q9,f) . l is set
m is set
(q9,f) . m is set
((q9,f)) is finite Element of bool NAT
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(q9) is finite Element of bool NAT
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(q9,f) . k1 is set
q9 . k1 is set
(q9,f) . k2 is set
q9 . k2 is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(q9) + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
j2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
f . j2 is set
ny . k1 is set
j + j2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny . (j + j2) is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(q9) + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
j2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
f . j2 is set
ny . k2 is set
j + j2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny . (j + j2) is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(q9) + k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
j2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(q9) + j2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
j1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
f . j1 is set
j2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
f . j2 is set
j + j1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny . (j + j1) is set
j + j2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny . (j + j2) is set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
((q9,(nx))) is finite Element of bool NAT
(q9) is finite Element of bool NAT
(q9,(nx)) . l is set
q9 . l is set
ny . l is set
((nx)) is finite Element of bool NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(q9) + m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
f . l is set
(q9) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((q9) + 1) + l is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
ny . (((q9) + 1) + l) is set
((q9) + ((nx))) + l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny . (((q9) + ((nx))) + l) is set
((q9,(nx))) + l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny . (((q9,(nx))) + l) is set
((q9,(nx)),f) is Relation-like NAT -defined Function-like finite () set
((nx)) + (q9) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(((nx)) + (q9)) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
1 + (q9) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(1 + (q9)) + (f) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(q9) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
1 + ((q9) + (f)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((q9,f)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
((q9,f)) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive 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) + ((nx)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(x) + 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 Relation-like NAT -defined Function-like finite () set
rng x is finite set
(x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
nx is set
(nx) is Relation-like NAT -defined Function-like finite () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(x,(nx)) is Relation-like NAT -defined Function-like finite () set
rng (x,(nx)) is finite set
ny is Relation-like NAT -defined Function-like finite () set
rng ny is finite set
((x,(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() Element of NAT
D is set
(D) is non empty 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)
F1() is non empty set
(F1()) is non empty set
D is set
f is set
x is Relation-like NAT -defined Function-like finite () set
x is Relation-like NAT -defined Function-like finite () set
nx is Relation-like NAT -defined Function-like finite () set
f is set
nx is Relation-like NAT -defined Function-like finite () set
x is set
({}) is Relation-like non-empty empty-yielding NAT -defined 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
(({})) is Relation-like non-empty empty-yielding NAT -defined 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 ({}) -element V43() complex-valued ext-real-valued real-valued natural-valued () 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 <= ({}) ) } is set
D is Relation-like Function-like set
f is Relation-like NAT -defined Function-like 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
{ 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 Relation-like Function-like () set
f is set
D | f is Relation-like Function-like set
dom D is set
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
{ 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 (D | f) is set
f |` D is Relation-like Function-like set
dom D is set
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
{ 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 (f |` D) is set
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
{ 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 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
{ 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
(0) is Relation-like non-empty empty-yielding NAT -defined 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 0 -element V43() complex-valued ext-real-valued real-valued natural-valued () () 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 <= 0 ) } is set
x is set
(NAT) is Relation-like non-empty empty-yielding NAT -defined NAT -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 () () ( NAT )
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
rng (NAT) is Relation-like non-empty empty-yielding NAT -defined 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
((NAT)) is Relation-like non-empty empty-yielding NAT -defined 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
nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
ny is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(NAT) . nx is Relation-like non-empty empty-yielding NAT -defined 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
j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(NAT) . ny is Relation-like non-empty empty-yielding NAT -defined 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
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
{ 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 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((x + 1)) is non empty finite x + 1 -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 + 1 ) } is set
nx is set
ny is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
{(x + 1)} is non empty trivial finite V39() 1 -element set
nx \ {(x + 1)} is Element of bool nx
bool nx is non empty set
x8 is set
x9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x8 is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
rng x8 is finite set
(x8) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(NAT,(x9 + 1)) is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
[1,(x9 + 1)] is set
{1,(x9 + 1)} is non empty finite V39() set
{{1,(x9 + 1)},{1}} is non empty finite V39() set
{[1,(x9 + 1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(NAT,x8,(NAT,(x9 + 1))) is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
p is Relation-like NAT -defined Function-like finite () () set
{(x9 + 1)} is non empty trivial finite V39() 1 -element set
p17 is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
rng p17 is finite set
rng (NAT,(x9 + 1)) is finite set
(rng x8) \/ (rng (NAT,(x9 + 1))) is finite set
(nx \ {(x + 1)}) \/ {(x9 + 1)} is non empty set
nx \/ {(x9 + 1)} is non empty set
(p17) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
q9 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
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
p17 . q9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
p17 . f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
((NAT,x8,(NAT,(x9 + 1)))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
((NAT,(x9 + 1))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(x8) + ((NAT,(x9 + 1))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(x8) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((x8)) is finite (x8) -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 <= (x8) ) } is set
(x8) is finite Element of bool NAT
x8 . q9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(NAT,x8,(NAT,(x9 + 1))) . ((x8) + ((NAT,(x9 + 1)))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(NAT,x8,(NAT,(x9 + 1))) . ((x8) + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
x8 . f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
ny is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
rng ny is finite set
(ny) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
rng x is finite set
(x) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
nx is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
rng nx is finite set
(nx) 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 NAT -defined 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
ny is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(k) is finite k -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 <= k ) } is set
j is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
rng j is finite set
(j) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny is Relation-like NAT -defined Function-like finite () () set
rng ny is finite set
(ny) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
k is set
(k) is Relation-like NAT -defined Function-like finite () () set
[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V39() set
{[1,k]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(ny,(k)) is Relation-like NAT -defined Function-like finite () () set
rng (ny,(k)) is finite set
((ny,(k))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
j is set
x8 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(x8) is finite x8 -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 <= x8 ) } is set
x9 is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
rng x9 is finite set
(x9) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
((k)) is finite Element of bool NAT
rng (k) is finite set
{k} is non empty trivial finite 1 -element set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
p17 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
((ny,(k))) is finite Element of bool NAT
q9 is set
(ny,(k)) . q9 is set
(((ny,(k)))) is finite ((ny,(k))) -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 <= ((ny,(k))) ) } is set
f 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() Element of NAT
(ny) + ((k)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(ny) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(ny,(k)) . f is set
(k) . 1 is set
(ny,(k)) . ((ny) + 1) is set
(ny,(k)) . ((ny) + ((k))) is set
(ny,(k)) . ((ny,(k))) is set
p17 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
((k)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(ny) + ((k)) 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
p17 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
p17 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
q9 is Relation-like NAT -defined Function-like finite () () set
(q9) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(q9) is finite Element of bool NAT
q9 is Relation-like NAT -defined Function-like finite () () set
(q9) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(q9) is finite Element of bool NAT
f is set
rng q9 is finite set
l is set
q9 . l is set
((q9)) is finite (q9) -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 <= (q9) ) } is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
((p17 + 1)) is non empty finite p17 + 1 -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 <= p17 + 1 ) } is set
(x9) is finite Element of bool NAT
x9 . m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
((k)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(q9) + ((k)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(((q9) + ((k)))) is finite (q9) + ((k)) -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 <= (q9) + ((k)) ) } is set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(q9) + l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x9 . ((q9) + l) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(k) . l is set
x9 . (x9) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
{k} is non empty trivial finite 1 -element set
rng (k) is finite set
(rng ny) \/ (rng (k)) is finite set
k1 is set
x9 . k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
((x9)) is finite (x9) -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 <= (x9) ) } is set
k2 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
(q9,(k)) is Relation-like NAT -defined Function-like finite () () set
{k} is non empty trivial finite 1 -element set
j \ {k} is Element of bool j
bool j is non empty set
(ny) is finite Element of bool NAT
l is set
ny . l is set
((ny)) is finite (ny) -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 <= (ny) ) } is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(ny) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(ny) + ((k)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(ny,(k)) . m is set
(ny,(k)) . ((ny) + 1) is set
rng (k) is finite set
(rng ny) \/ (rng (k)) is finite set
(rng ny) \/ {k} is non empty finite set
((rng ny) \/ {k}) \ {k} is finite Element of bool ((rng ny) \/ {k})
bool ((rng ny) \/ {k}) is non empty finite V39() set
l is set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
ny . l is set
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
ny . m is set
((ny)) is finite (ny) -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 <= (ny) ) } is set
(ny) is finite Element of bool NAT
(ny,(k)) . l is set
(ny,(k)) . m is 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
(ny) + ((k)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
f is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
rng f is finite set
(f) is finite Element of bool NAT
l is set
f . l 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() Element of 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
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(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) + ((k)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(f,(k)) is Relation-like NAT -defined Function-like finite () () set
((f,(k))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
x9 . m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
x9 . ((f) + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(rng f) \/ (rng (k)) is finite set
(rng f) \/ {k} is non empty finite set
((rng f) \/ {k}) \ {k} is finite Element of bool ((rng f) \/ {k})
bool ((rng f) \/ {k}) is non empty finite V39() set
l is set
(f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
k1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
f . l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
k2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
f . m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(p17) is finite p17 -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 <= p17 ) } is set
x9 . l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
x9 . m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(l) is finite l -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 <= l ) } is set
D is Relation-like NAT -defined Function-like () set
dom D is set
((dom D)) is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
rng ((dom D)) is finite 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
{ 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 Relation-like NAT -defined Function-like () set
dom D is set
((dom D)) is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
((dom D)) * D is Relation-like NAT -defined Function-like finite set
D is Relation-like NAT -defined Function-like () set
(D) is Relation-like Function-like set
dom D is set
((dom D)) is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
((dom D)) * D is Relation-like NAT -defined Function-like finite set
rng ((dom D)) is finite set
dom (((dom D)) * D) is finite set
(((dom D))) is finite Element of bool NAT
(((dom D))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
((((dom D)))) is finite (((dom 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 <= (((dom D))) ) } is set
D is set
(D) is Relation-like NAT -defined NAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
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
{ 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 finite set
D is set
f is Relation-like Function-like set
rng f is set
dom f is set
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
{ 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
nx is set
ny 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
1 + k is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
nx is Relation-like Function-like set
dom nx is set
rng nx 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 x <= b1 } is set
ny is set
k is set
nx . k is set
j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
j + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
ny is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
k + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
nx . (k + 1) is set
j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
j + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
nx * f is Relation-like Function-like set
dom (nx * f) is set
ny is Relation-like NAT -defined Function-like finite () () set
rng ny is finite set
f is Relation-like NAT -defined Function-like finite () () set
rng f is 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
(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
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : not x <= b1 } is set
nx is set
k 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
ny + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
nx is Relation-like Function-like set
dom nx is set
nx * f is Relation-like Function-like set
rng (nx * f) is set
dom (nx * f) is set
rng nx is set
ny is set
k is set
nx . k is set
j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
j + 1 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
ny is set
k is epsilon-transitive epsilon-connected ordinal natural ext-real 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
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
nx . x8 is set
x9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
x9 + 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 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 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
{ 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 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
{ 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
nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(nx) is finite nx -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 <= nx ) } is set
nx is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(nx) is finite nx -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 <= nx ) } is set
ny is Relation-like Function-like set
dom ny is set
rng ny 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 Relation-like Function-like set
dom k is set
rng k 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
x8 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x8 + 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() Element of NAT
j + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(x8) is finite x8 -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 <= x8 ) } is set
(j) is finite j -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 <= j ) } is set
{nx} is non empty trivial finite V39() 1 -element set
(x8) /\ {nx} is finite Element of bool NAT
x9 is set
{x} is non empty trivial finite V39() 1 -element set
(j) /\ {x} is finite Element of bool NAT
x9 is set
(x8) \/ {nx} is non empty finite set
(j) \/ {x} is non empty finite set
(x8) \ {nx} is finite Element of bool NAT
((x8) \/ {nx}) \ {nx} is finite Element of bool ((x8) \/ {nx})
bool ((x8) \/ {nx}) is non empty finite V39() set
(j) \ {x} is finite Element of bool NAT
((j) \/ {x}) \ {x} is finite Element of bool ((j) \/ {x})
bool ((j) \/ {x}) is non empty finite V39() set
(nx) \ {nx} is finite Element of bool NAT
(x) \ {x} is finite Element of bool NAT
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
{ 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 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
{ 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
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 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
{ 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 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
{ 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
card (D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of omega
D is set
(D) is Relation-like NAT -defined 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
(NAT,0) is Relation-like NAT -defined NAT -valued Function-like non empty finite complex-valued ext-real-valued real-valued natural-valued () () ( NAT )
[1,0] is set
{1,0} is non empty finite V39() set
{{1,0},{1}} is non empty finite V39() set
{[1,0]} is Relation-like Function-like constant non empty trivial finite 1 -element set
D is Relation-like NAT -defined Function-like finite () () set
f is Relation-like NAT -defined Function-like non empty finite () () set
(D,f) is Relation-like NAT -defined Function-like finite () () set
(f,D) is Relation-like NAT -defined Function-like finite () () set
D is set
f is set
(D,f) is Relation-like NAT -defined Function-like finite () () set
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
x is set
(D,f,x) is Relation-like NAT -defined Function-like finite () () set
(x) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
F2() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(F2()) is finite F2() -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 <= F2() ) } is set
F1() is non empty set
D is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x is Element of F1()
D is Relation-like Function-like set
dom D is set
rng D is set
f is Relation-like NAT -defined Function-like finite () () set
x is Relation-like NAT -defined F1() -valued Function-like finite () () (F1())
(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
x . nx is set
f is Relation-like NAT -defined Function-like finite () () 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
{ 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 | (D) is Relation-like (D) -defined NAT -defined Function-like finite () set
D is set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
x is Relation-like NAT -defined D -valued Function-like finite () () (D)
(f,x) is Relation-like NAT -defined Function-like 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 | (f) is Relation-like (f) -defined NAT -defined D -valued Function-like finite () set
D is Relation-like NAT -defined Function-like finite () () set
(0,D) is Relation-like NAT -defined Function-like finite () () set
(0) is Relation-like non-empty empty-yielding NAT -defined 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 0 -element V43() complex-valued ext-real-valued real-valued natural-valued () () 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 <= 0 ) } is set
D | (0) is Relation-like non-empty empty-yielding NAT -defined (0) -defined NAT -defined 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
f is Relation-like NAT -defined 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 Relation-like NAT -defined Function-like 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
f | (D) is Relation-like (D) -defined NAT -defined Function-like 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
(f) is finite Element of bool NAT
D is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
f is Relation-like NAT -defined 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 Relation-like NAT -defined Function-like 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
f | (D) is Relation-like (D) -defined NAT -defined 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 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 finite Element of bool 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 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
D + x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
f + x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
((f + x)) is finite 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 <= f + x ) } is set
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 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
D + x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
f + x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
((f + x)) is finite 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 <= f + x ) } is set
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 Relation-like set
field D is set
dom D is set
rng D is set
(dom D) \/ (rng D) is set
f is Relation-like set
x is Relation-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
k is Relation-like NAT -defined Function-like finite () () set
(k) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
k . 1 is set
k . (k) is set
k is Relation-like NAT -defined Function-like finite () () set
(k) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
k . 1 is set
k . (k) is set
D is set
f is set
(D) is non empty set
(f) is non empty set
x is set
nx is Relation-like NAT -defined D -valued Function-like finite () () (D)
rng nx is finite set
D is set
(D) is non empty set
f is set
D is Relation-like NAT -defined Function-like finite () () set
f is Relation-like NAT -defined 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
card D 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 NAT -defined 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 NAT -defined Function-like finite () () set
(D,f) is Relation-like NAT -defined 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
D . 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
(D) is finite Element of bool NAT
f is Relation-like NAT -defined 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 NAT -defined Function-like finite () () set
(D,f) is Relation-like NAT -defined Function-like finite () () set
(D) 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) + x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(D,f) . ((D) + x) is set
f . x 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
(D) + (f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
((D) + x) - (D) is ext-real V33() complex V43() set
f . (((D) + x) - (D)) is set
F1() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
F2() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
{ F3(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT : ( F1() <= b1 & b1 <= F2() & P1[b1] ) } is set
F2() + 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 NAT -defined 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
rng f is 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
F3(nx) is set
nx + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((F2() + 1)) is non empty finite F2() + 1 -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 <= F2() + 1 ) } is set
f . (nx + 1) is set
(nx + 1) - 1 is ext-real V33() complex V43() set
F3(((nx + 1) - 1)) is set
(3) is non empty finite 3 -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 <= 3 ) } is set
4 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(4) is non empty finite 4 -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 <= 4 ) } is set
5 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(5) is non empty finite 5 -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 <= 5 ) } is set
6 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(6) is non empty finite 6 -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 <= 6 ) } is set
7 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(7) is non empty finite 7 -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 <= 7 ) } is set
8 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(8) is non empty finite 8 -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 <= 8 ) } is set
D is set
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
x is set
(x) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
nx is set
(nx) is Relation-like NAT -defined Function-like non empty finite () () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((D),(f)),(x)),(nx)) is Relation-like NAT -defined Function-like non empty finite () () set
ny is Relation-like NAT -defined Function-like finite () () set
(ny) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
ny . 1 is set
ny . 2 is set
ny . 3 is set
ny . 4 is set
(D,f,x) is Relation-like NAT -defined Function-like non empty finite () () set
((((D),(f)),(x))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((D),(f)),(x)) . 1 is set
(((D),(f)),(x)) . 2 is set
(((D),(f)),(x)) . 3 is set
((nx)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((D),(f)),(x))) + ((nx)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((D),(f)),(x))) is non empty finite Element of bool NAT
((((D),(f)),(x))) + 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),(f)),(x))) + 1) is set
D is set
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
x is set
(x) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
nx is set
(nx) is Relation-like NAT -defined Function-like non empty finite () () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((D),(f)),(x)),(nx)) is Relation-like NAT -defined Function-like non empty finite () () set
ny is set
(ny) is Relation-like NAT -defined Function-like non empty finite () () set
[1,ny] is set
{1,ny} is non empty finite set
{{1,ny},{1}} is non empty finite V39() set
{[1,ny]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((((D),(f)),(x)),(nx)),(ny)) is Relation-like NAT -defined Function-like non empty finite () () set
k is Relation-like NAT -defined Function-like finite () () set
(k) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
k . 1 is set
k . 2 is set
k . 3 is set
k . 4 is set
k . 5 is set
(((((D),(f)),(x)),(nx))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((D),(f)),(x)),(nx)) . 1 is set
((((D),(f)),(x)),(nx)) . 2 is set
((((D),(f)),(x)),(nx)) . 3 is set
((((D),(f)),(x)),(nx)) . 4 is set
((ny)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((((D),(f)),(x)),(nx))) + ((ny)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
4 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((((D),(f)),(x)),(nx))) is non empty finite Element of bool NAT
(((((D),(f)),(x)),(nx))) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
k . ((((((D),(f)),(x)),(nx))) + 1) is set
D is set
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
x is set
(x) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
nx is set
(nx) is Relation-like NAT -defined Function-like non empty finite () () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((D),(f)),(x)),(nx)) is Relation-like NAT -defined Function-like non empty finite () () set
ny is set
(ny) is Relation-like NAT -defined Function-like non empty finite () () set
[1,ny] is set
{1,ny} is non empty finite set
{{1,ny},{1}} is non empty finite V39() set
{[1,ny]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((((D),(f)),(x)),(nx)),(ny)) is Relation-like NAT -defined Function-like non empty finite () () set
k is set
(k) is Relation-like NAT -defined Function-like non empty finite () () set
[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V39() set
{[1,k]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((((D),(f)),(x)),(nx)),(ny)),(k)) is Relation-like NAT -defined Function-like non empty finite () () set
j is Relation-like NAT -defined Function-like finite () () set
(j) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
j . 1 is set
j . 2 is set
j . 3 is set
j . 4 is set
j . 5 is set
j . 6 is set
((((((D),(f)),(x)),(nx)),(ny))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((((D),(f)),(x)),(nx)),(ny)) . 1 is set
(((((D),(f)),(x)),(nx)),(ny)) . 2 is set
(((((D),(f)),(x)),(nx)),(ny)) . 3 is set
(((((D),(f)),(x)),(nx)),(ny)) . 4 is set
(((((D),(f)),(x)),(nx)),(ny)) . 5 is set
((k)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((((D),(f)),(x)),(nx)),(ny))) + ((k)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
5 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((((D),(f)),(x)),(nx)),(ny))) is non empty finite Element of bool NAT
((((((D),(f)),(x)),(nx)),(ny))) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
j . (((((((D),(f)),(x)),(nx)),(ny))) + 1) is set
D is set
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
x is set
(x) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
nx is set
(nx) is Relation-like NAT -defined Function-like non empty finite () () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((D),(f)),(x)),(nx)) is Relation-like NAT -defined Function-like non empty finite () () set
ny is set
(ny) is Relation-like NAT -defined Function-like non empty finite () () set
[1,ny] is set
{1,ny} is non empty finite set
{{1,ny},{1}} is non empty finite V39() set
{[1,ny]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((((D),(f)),(x)),(nx)),(ny)) is Relation-like NAT -defined Function-like non empty finite () () set
k is set
(k) is Relation-like NAT -defined Function-like non empty finite () () set
[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V39() set
{[1,k]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((((D),(f)),(x)),(nx)),(ny)),(k)) is Relation-like NAT -defined Function-like non empty finite () () set
j is set
(j) is Relation-like NAT -defined Function-like non empty finite () () set
[1,j] is set
{1,j} is non empty finite set
{{1,j},{1}} is non empty finite V39() set
{[1,j]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) is Relation-like NAT -defined Function-like non empty finite () () set
x8 is Relation-like NAT -defined Function-like finite () () set
(x8) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x8 . 1 is set
x8 . 2 is set
x8 . 3 is set
x8 . 4 is set
x8 . 5 is set
x8 . 6 is set
x8 . 7 is set
(((((((D),(f)),(x)),(nx)),(ny)),(k))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((((D),(f)),(x)),(nx)),(ny)),(k)) . 1 is set
((((((D),(f)),(x)),(nx)),(ny)),(k)) . 2 is set
((((((D),(f)),(x)),(nx)),(ny)),(k)) . 3 is set
((((((D),(f)),(x)),(nx)),(ny)),(k)) . 4 is set
((((((D),(f)),(x)),(nx)),(ny)),(k)) . 5 is set
((((((D),(f)),(x)),(nx)),(ny)),(k)) . 6 is set
((j)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((((((D),(f)),(x)),(nx)),(ny)),(k))) + ((j)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
6 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((((((D),(f)),(x)),(nx)),(ny)),(k))) is non empty finite Element of bool NAT
(((((((D),(f)),(x)),(nx)),(ny)),(k))) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
x8 . ((((((((D),(f)),(x)),(nx)),(ny)),(k))) + 1) is set
D is set
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
x is set
(x) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
nx is set
(nx) is Relation-like NAT -defined Function-like non empty finite () () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((D),(f)),(x)),(nx)) is Relation-like NAT -defined Function-like non empty finite () () set
ny is set
(ny) is Relation-like NAT -defined Function-like non empty finite () () set
[1,ny] is set
{1,ny} is non empty finite set
{{1,ny},{1}} is non empty finite V39() set
{[1,ny]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((((D),(f)),(x)),(nx)),(ny)) is Relation-like NAT -defined Function-like non empty finite () () set
k is set
(k) is Relation-like NAT -defined Function-like non empty finite () () set
[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V39() set
{[1,k]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((((D),(f)),(x)),(nx)),(ny)),(k)) is Relation-like NAT -defined Function-like non empty finite () () set
j is set
(j) is Relation-like NAT -defined Function-like non empty finite () () set
[1,j] is set
{1,j} is non empty finite set
{{1,j},{1}} is non empty finite V39() set
{[1,j]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) is Relation-like NAT -defined Function-like non empty finite () () set
x8 is set
(x8) is Relation-like NAT -defined Function-like non empty finite () () set
[1,x8] is set
{1,x8} is non empty finite set
{{1,x8},{1}} is non empty finite V39() set
{[1,x8]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) is Relation-like NAT -defined Function-like non empty finite () () set
x9 is Relation-like NAT -defined Function-like finite () () set
(x9) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
x9 . 1 is set
x9 . 2 is set
x9 . 3 is set
x9 . 4 is set
x9 . 5 is set
x9 . 6 is set
x9 . 7 is set
x9 . 8 is set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) . 1 is set
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) . 2 is set
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) . 3 is set
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) . 4 is set
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) . 5 is set
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) . 6 is set
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) . 7 is set
((x8)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j))) + ((x8)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
7 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j))) is non empty finite Element of bool NAT
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j))) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
x9 . (((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j))) + 1) is set
9 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
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
x is set
(x) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
nx is set
(nx) is Relation-like NAT -defined Function-like non empty finite () () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((D),(f)),(x)),(nx)) is Relation-like NAT -defined Function-like non empty finite () () set
ny is set
(ny) is Relation-like NAT -defined Function-like non empty finite () () set
[1,ny] is set
{1,ny} is non empty finite set
{{1,ny},{1}} is non empty finite V39() set
{[1,ny]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((((D),(f)),(x)),(nx)),(ny)) is Relation-like NAT -defined Function-like non empty finite () () set
k is set
(k) is Relation-like NAT -defined Function-like non empty finite () () set
[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V39() set
{[1,k]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((((D),(f)),(x)),(nx)),(ny)),(k)) is Relation-like NAT -defined Function-like non empty finite () () set
j is set
(j) is Relation-like NAT -defined Function-like non empty finite () () set
[1,j] is set
{1,j} is non empty finite set
{{1,j},{1}} is non empty finite V39() set
{[1,j]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)) is Relation-like NAT -defined Function-like non empty finite () () set
x8 is set
(x8) is Relation-like NAT -defined Function-like non empty finite () () set
[1,x8] is set
{1,x8} is non empty finite set
{{1,x8},{1}} is non empty finite V39() set
{[1,x8]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) is Relation-like NAT -defined Function-like non empty finite () () set
x9 is set
(x9) is Relation-like NAT -defined Function-like non empty finite () () set
[1,x9] is set
{1,x9} is non empty finite set
{{1,x9},{1}} is non empty finite V39() set
{[1,x9]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)),(x9)) is Relation-like NAT -defined Function-like non empty finite () () set
p is Relation-like NAT -defined Function-like finite () () set
(p) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
p . 1 is set
p . 2 is set
p . 3 is set
p . 4 is set
p . 5 is set
p . 6 is set
p . 7 is set
p . 8 is set
p . 9 is set
(((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) . 1 is set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) . 2 is set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) . 3 is set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) . 4 is set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) . 5 is set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) . 6 is set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) . 7 is set
((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8)) . 8 is set
((x9)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8))) + ((x9)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
8 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8))) is non empty finite Element of bool NAT
(((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8))) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
p . ((((((((((D),(f)),(x)),(nx)),(ny)),(k)),(j)),(x8))) + 1) is set
D is Relation-like NAT -defined Function-like finite () () set
((0),D) is Relation-like NAT -defined Function-like finite () () set
((0)) is Relation-like non-empty empty-yielding NAT -defined 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 (0) -element V43() complex-valued ext-real-valued real-valued natural-valued () () 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 <= (0) ) } is set
D | ((0)) is Relation-like non-empty empty-yielding NAT -defined ((0)) -defined NAT -defined 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 Relation-like NAT -defined Function-like finite () () set
((0),D) is Relation-like NAT -defined Function-like finite () () set
((0)) is Relation-like non-empty empty-yielding NAT -defined 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 (0) -element V43() complex-valued ext-real-valued real-valued natural-valued () () 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 <= (0) ) } is set
D | ((0)) is Relation-like non-empty empty-yielding NAT -defined ((0)) -defined NAT -defined 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
f is Relation-like NAT -defined Function-like finite () () set
((0),f) is Relation-like NAT -defined Function-like finite () () set
f | ((0)) is Relation-like non-empty empty-yielding NAT -defined ((0)) -defined NAT -defined 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 non empty set
f is Element of D
(D,f) is Relation-like NAT -defined D -valued Function-like non empty finite () () (D)
[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 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)
(D,f,x) is Relation-like NAT -defined D -valued Function-like finite () () (D)
D is set
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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) . 1 is set
D is set
f is set
(D,f) is Relation-like NAT -defined Function-like non empty finite () () set
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
x is set
nx is set
(x,nx) is Relation-like NAT -defined Function-like non empty finite () () set
(x) is Relation-like NAT -defined Function-like non empty 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
(nx) is Relation-like NAT -defined Function-like non empty finite () () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((x),(nx)) is Relation-like NAT -defined Function-like non empty finite () () set
(D,f) . 1 is set
(D,f) . 2 is set
D is set
f is set
x is set
(D,f,x) is Relation-like NAT -defined Function-like non empty finite () () set
(D) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
(x) is Relation-like NAT -defined Function-like non empty 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 NAT -defined Function-like non empty finite () () set
nx is set
ny is set
k is set
(nx,ny,k) is Relation-like NAT -defined Function-like non empty finite () () set
(nx) is Relation-like NAT -defined Function-like non empty finite () () set
[1,nx] is set
{1,nx} is non empty finite set
{{1,nx},{1}} is non empty finite V39() set
{[1,nx]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(ny) is Relation-like NAT -defined Function-like non empty finite () () set
[1,ny] is set
{1,ny} is non empty finite set
{{1,ny},{1}} is non empty finite V39() set
{[1,ny]} is Relation-like Function-like constant non empty trivial finite 1 -element set
((nx),(ny)) is Relation-like NAT -defined Function-like non empty finite () () set
(k) is Relation-like NAT -defined Function-like non empty finite () () set
[1,k] is set
{1,k} is non empty finite set
{{1,k},{1}} is non empty finite V39() set
{[1,k]} is Relation-like Function-like constant non empty trivial finite 1 -element set
(((nx),(ny)),(k)) is Relation-like NAT -defined Function-like non empty finite () () set
(D,f,x) . 1 is set
(D,f,x) . 2 is set
(D,f,x) . 3 is set
{{}} is functional non empty trivial finite V39() 1 -element set
({{}}) is Relation-like NAT -defined Function-like non empty finite () () set
[1,{{}}] is set
{1,{{}}} is non empty finite V39() set
{{1,{{}}},{1}} is non empty finite V39() set
{[1,{{}}]} is Relation-like Function-like constant non empty trivial finite 1 -element set
rng ({{}}) is non empty finite set
{{{}}} is non empty trivial finite V39() 1 -element 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
{ 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 Relation-like NAT -defined Function-like finite () () set
f is Relation-like NAT -defined Function-like finite () () set
f | (D) is Relation-like (D) -defined NAT -defined Function-like finite () set
(x) 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
(x) is finite Element of bool NAT
(f) is finite Element of bool NAT
(f) /\ (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
((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 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
{ 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 Relation-like NAT -defined Function-like finite () () set
f is Relation-like NAT -defined Function-like finite () () set
f | (D) is Relation-like (D) -defined NAT -defined Function-like finite () set
(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
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
ny is Relation-like NAT -defined Function-like finite () () set
(ny) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(ny) is finite Element of bool NAT
(x,ny) is Relation-like NAT -defined Function-like finite () () set
((x,ny)) 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
((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
(x,ny) . k is set
x . k is set
f . k is set
j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() set
(x) + j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
k - (x) is ext-real V33() complex V43() set
ny . j is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(nx) is finite nx -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 <= nx ) } is set
D is non empty set
the Element of D is Element of D
(D, the Element of D) is Relation-like NAT -defined D -valued Function-like non empty finite () () (D)
[1, the Element of D] is set
{1, the Element of D} is non empty finite set
{{1, the Element of D},{1}} is non empty finite V39() set
{[1, the Element of D]} is Relation-like Function-like constant non empty trivial finite 1 -element set
D is Relation-like NAT -defined Function-like finite () () set
f is Relation-like NAT -defined 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
x 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 set
card D is epsilon-transitive epsilon-connected ordinal cardinal set
f is set
card f is epsilon-transitive epsilon-connected ordinal cardinal set
D is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() set
(D) is non empty 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 Relation-like NAT -defined Function-like finite () () set
x 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,D) is Relation-like NAT -defined Function-like 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
D | (f) is Relation-like (f) -defined NAT -defined Function-like finite () set
(x,(f,D)) is Relation-like NAT -defined Function-like finite () () 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
(f,D) | (x) is Relation-like (x) -defined NAT -defined Function-like finite () set
(x,D) is Relation-like NAT -defined Function-like finite () () set
D | (x) is Relation-like (x) -defined NAT -defined Function-like finite () set
{0} is functional non empty trivial finite V39() 1 -element 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
{ 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 epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V33() complex finite cardinal V43() Element of NAT
(D + 1) \ {0} is finite Element of bool (D + 1)
bool (D + 1) is non empty finite V39() 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 + 1 <= b1 } 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
f is set
x is epsilon-transitive epsilon-connected ordinal natural ext-real 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 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
{ 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 Relation-like (D) -defined INT -valued {{}} -valued Function-like V25((D),{{}}) finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(D),{{}}:]
{{}} is functional non empty trivial finite V39() 1 -element set
[:(D),{{}}:] is Relation-like finite set
bool [:(D),{{}}:] is non empty finite V39() set
dom ((D) --> {}) is finite set
x is Relation-like NAT -defined 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 (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 is set
(D) is Relation-like NAT -defined Function-like non empty 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
(D,f) is Relation-like NAT -defined Function-like non empty finite () () set
(f) is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element () () 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 NAT -defined Function-like non empty finite () () set
((D,f)) 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
(D,f,x) is Relation-like NAT -defined Function-like non empty finite () () set
(x) is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element () () 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 NAT -defined Function-like non empty finite () () set
((D,f,x)) 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
f is set
the Relation-like NAT -defined Function-like finite () () set is Relation-like NAT -defined Function-like finite () () set
{ the Relation-like NAT -defined Function-like finite () () set } is functional non empty trivial finite V39() 1 -element set
D is functional non empty trivial finite V39() 1 -element set
f is set
D is set
(D) is functional non empty set
f is set
D is set
f is set
(f) is functional non empty () set
x is Relation-like Function-like set
dom x is set
x . D is set
rng x is set
D is set
f is set
D is functional () set
{ (rng b1) where b1 is Relation-like Function-like Element of D : b1 in D } is set
union { (rng b1) where b1 is Relation-like Function-like Element of D : b1 in D } is set
succ (union { (rng b1) where b1 is Relation-like Function-like Element of D : b1 in D } ) is non empty set
x is non empty set
(x) is functional non empty () set
nx is set
ny is Relation-like NAT -defined Function-like finite () () set
rng ny is finite set
D is functional () set
f is Relation-like Function-like Element of D
D is functional () set
bool D is non empty set
f is functional Element of bool D
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
{ 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 Relation-like NAT -defined Function-like finite () () set
f is Relation-like NAT -defined Function-like finite () () set
f | (D) is Relation-like (D) -defined NAT -defined 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 Element of bool NAT
(f) /\ (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
D is Relation-like NAT -defined Function-like finite () () set
f is Relation-like NAT -defined Function-like finite () () set
(D,f) is Relation-like NAT -defined Function-like finite () () set
(f,D) is Relation-like NAT -defined 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
((f,D)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
(f) + (D) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V33() complex finite cardinal V43() Element of NAT
D is set
(D) is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element () () 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 NAT -defined Function-like finite () () set
x is Relation-like NAT -defined Function-like finite () () set
(f,x) is Relation-like NAT -defined Function-like finite () () set
((f,x)) 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
(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
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 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
{ 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 Relation-like NAT -defined Function-like finite D -element () () set
(f) is finite D -element Element of bool NAT
(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() 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
x is Relation-like NAT -defined Function-like finite D -element () () set
nx is Relation-like NAT -defined Function-like finite f -element () () set
(x,nx) is Relation-like NAT -defined Function-like finite () () set
(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() Element of NAT
((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 NAT -defined Function-like finite complex-valued ext-real-valued real-valued () () set
f is set
dom D is finite set
x is set
D . f is ext-real V33() complex set
D . x is ext-real V33() complex set
(D) is finite Element of bool NAT
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() Element of NAT
D is set
f is set
(f) is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element () () 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
((f)) is non empty trivial finite 1 -element Element of bool NAT
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 functional () set
f is Relation-like D -valued Function-like set
x is set
f . x is Relation-like Function-like set
dom f is set
rng f is set
dom f is set
dom f is set