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