REAL is set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal countable denumerable non empty-membered Element of bool REAL
bool REAL is non empty cup-closed diff-closed preBoolean set
RAT 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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued set
the 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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued 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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal countable denumerable non empty-membered set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite non empty-membered set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite non empty-membered set
Fin NAT is non empty cup-closed diff-closed preBoolean set
COMPLEX is set
INT is set
1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
{{},1} is non empty finite V40() countable set
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty cup-closed diff-closed preBoolean set
K462() is set
bool K462() is non empty cup-closed diff-closed preBoolean set
K463() is Element of bool K462()
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is non empty cup-closed diff-closed preBoolean set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty cup-closed diff-closed preBoolean set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is non empty cup-closed diff-closed preBoolean set
[:RAT,RAT:] is Relation-like set
bool [:RAT,RAT:] is non empty cup-closed diff-closed preBoolean set
[:[:RAT,RAT:],RAT:] is Relation-like set
bool [:[:RAT,RAT:],RAT:] is non empty cup-closed diff-closed preBoolean set
[:INT,INT:] is Relation-like set
bool [:INT,INT:] is non empty cup-closed diff-closed preBoolean set
[:[:INT,INT:],INT:] is Relation-like set
bool [:[:INT,INT:],INT:] is non empty cup-closed diff-closed preBoolean set
[:NAT,NAT:] is Relation-like non empty non trivial non finite non empty-membered set
[:[:NAT,NAT:],NAT:] is Relation-like non empty non trivial non finite non empty-membered set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial cup-closed diff-closed preBoolean non finite non empty-membered set
K576() is set
2 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of NAT
Seg 1 is non empty trivial finite 1 -element countable Element of bool NAT
{1} is non empty trivial finite V40() 1 -element countable with_non-empty_elements non empty-membered set
Seg 2 is non empty finite 2 -element countable Element of bool NAT
{1,2} is non empty finite V40() countable with_non-empty_elements non empty-membered set
dom {} 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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V77() set
rng {} 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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V72() V73() V74() V75() V77() with_non-empty_elements set
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued FinSequence of REAL
K430((<*> REAL)) is V55() real ext-real Element of REAL
{{}} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
addnat is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total commutative associative having_a_unity complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
multnat is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total commutative associative having_a_unity complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
the_unity_wrt multnat is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
D is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
M is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
D ^ M is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
D ^ M is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of k
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
<*> k is Relation-like non-empty empty-yielding NAT -defined k -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued FinSequence of k
k is set
<*> k is Relation-like non-empty empty-yielding NAT -defined k -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued FinSequence of k
k * is functional non empty FinSequence-membered FinSequenceSet of k
k is non empty set
D is Element of k
<*D*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like set
k * is functional non empty FinSequence-membered FinSequenceSet of k
<*D*> is Relation-like NAT -defined k -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of k
M is Element of k
<*D,M*> is Relation-like NAT -defined Function-like non empty finite 2 -element countable FinSequence-like FinSubsequence-like set
<*D,M*> is Relation-like NAT -defined k -valued Function-like non empty finite 2 -element countable FinSequence-like FinSubsequence-like FinSequence of k
<*D*> is Relation-like NAT -defined k -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of k
<*M*> is Relation-like NAT -defined k -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like FinSequence of k
<*D*> ^ <*M*> is Relation-like NAT -defined k -valued Function-like non empty finite 1 + 1 -element countable FinSequence-like FinSubsequence-like FinSequence of k
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
D is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
[:(k *),(k *):] is Relation-like non empty set
[:[:(k *),(k *):],(k *):] is Relation-like non empty set
bool [:[:(k *),(k *):],(k *):] is non empty cup-closed diff-closed preBoolean set
D is Relation-like NAT -defined k * -valued Function-like finite countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence of k *
M is Relation-like [:(k *),(k *):] -defined k * -valued Function-like non empty total quasi_total Function-yielding V50() Element of bool [:[:(k *),(k *):],(k *):]
M "**" D is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
i is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
M . (x,i) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[x,i] is set
{x,i} is functional non empty finite V40() countable set
{x} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{x,i},{x}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
M . [x,i] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
(k,x,i) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
M is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
i is Relation-like [:(k *),(k *):] -defined k * -valued Function-like non empty total quasi_total Function-yielding V50() Element of bool [:[:(k *),(k *):],(k *):]
i "**" D is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
Fg is Relation-like [:(k *),(k *):] -defined k * -valued Function-like non empty total quasi_total Function-yielding V50() Element of bool [:[:(k *),(k *):],(k *):]
Fg "**" D is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
db is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
k1 is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
i . (db,k1) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[db,k1] is set
{db,k1} is functional non empty finite V40() countable set
{db} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{db,k1},{db}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
i . [db,k1] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
(k,db,k1) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
Fg . (db,k1) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
Fg . [db,k1] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
D is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
((k *),D) is Relation-like NAT -defined k * -valued Function-like constant non empty trivial finite 1 -element countable Function-yielding V50() FinSequence-like FinSubsequence-like Element of (k *) *
(k *) * is functional non empty FinSequence-membered FinSequenceSet of k *
(k,((k *),D)) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[:(k *),(k *):] is Relation-like non empty set
[:[:(k *),(k *):],(k *):] is Relation-like non empty set
bool [:[:(k *),(k *):],(k *):] is non empty cup-closed diff-closed preBoolean set
M is Relation-like [:(k *),(k *):] -defined k * -valued Function-like non empty total quasi_total Function-yielding V50() Element of bool [:[:(k *),(k *):],(k *):]
M "**" ((k *),D) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
((k *)) is Relation-like non-empty empty-yielding NAT -defined k * -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of (k *) *
(k *) * is functional non empty FinSequence-membered FinSequenceSet of k *
(k,((k *))) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k) is Relation-like non-empty empty-yielding NAT -defined k -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of k *
[:(k *),(k *):] is Relation-like non empty set
[:[:(k *),(k *):],(k *):] is Relation-like non empty set
bool [:[:(k *),(k *):],(k *):] is non empty cup-closed diff-closed preBoolean set
D is Relation-like [:(k *),(k *):] -defined k * -valued Function-like non empty total quasi_total Function-yielding V50() Element of bool [:[:(k *),(k *):],(k *):]
D "**" ((k *)) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
D . ({},x) is set
[{},x] is set
{{},x} is functional non empty finite V40() countable set
{{{},x},{{}}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
D . [{},x] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
{} ^ x is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
D . (x,{}) is set
[x,{}] is set
{x,{}} is functional non empty finite V40() countable set
{x} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{x,{}},{x}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
D . [x,{}] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
x ^ {} is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
M is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
the_unity_wrt D is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
D is Relation-like NAT -defined k * -valued Function-like finite countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence of k *
M is Relation-like NAT -defined k * -valued Function-like finite countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence of k *
D ^ M is Relation-like NAT -defined k * -valued Function-like finite countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence of k *
(k,(D ^ M)) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,D) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,M) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,(k,D),(k,M)) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[:(k *),(k *):] is Relation-like non empty set
[:[:(k *),(k *):],(k *):] is Relation-like non empty set
bool [:[:(k *),(k *):],(k *):] is non empty cup-closed diff-closed preBoolean set
x is Relation-like [:(k *),(k *):] -defined k * -valued Function-like non empty total quasi_total Function-yielding V50() Element of bool [:[:(k *),(k *):],(k *):]
x "**" (D ^ M) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
i is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
Fg is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
db is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x . (Fg,db) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[Fg,db] is set
{Fg,db} is functional non empty finite V40() countable set
{Fg} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{Fg,db},{Fg}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x . [Fg,db] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
x . (i,(x . (Fg,db))) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[i,(x . (Fg,db))] is set
{i,(x . (Fg,db))} is functional non empty finite V40() countable set
{i} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{i,(x . (Fg,db))},{i}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x . [i,(x . (Fg,db))] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
(k,i,(x . (Fg,db))) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,Fg,db) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,i,(k,Fg,db)) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,i,Fg) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,(k,i,Fg),db) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x . (i,Fg) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[i,Fg] is set
{i,Fg} is functional non empty finite V40() countable set
{{i,Fg},{i}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x . [i,Fg] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
(k,(x . (i,Fg)),db) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x . ((x . (i,Fg)),db) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[(x . (i,Fg)),db] is set
{(x . (i,Fg)),db} is functional non empty finite V40() countable set
{(x . (i,Fg))} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{(x . (i,Fg)),db},{(x . (i,Fg))}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x . [(x . (i,Fg)),db] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
Fg is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x . ({},Fg) is set
[{},Fg] is set
{{},Fg} is functional non empty finite V40() countable set
{{{},Fg},{{}}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x . [{},Fg] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
{} ^ Fg is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
x . (Fg,{}) is set
[Fg,{}] is set
{Fg,{}} is functional non empty finite V40() countable set
{Fg} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{Fg,{}},{Fg}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x . [Fg,{}] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
Fg ^ {} is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
i is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
len D is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
len M is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
x "**" D is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x "**" M is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x . ((x "**" D),(x "**" M)) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[(x "**" D),(x "**" M)] is set
{(x "**" D),(x "**" M)} is functional non empty finite V40() countable set
{(x "**" D)} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{(x "**" D),(x "**" M)},{(x "**" D)}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x . [(x "**" D),(x "**" M)] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
(k,(x "**" D),(x "**" M)) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,(k,D),(x "**" M)) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
D is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
M is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
((k *),D,M) is Relation-like NAT -defined k * -valued Function-like non empty finite 2 -element countable Function-yielding V50() FinSequence-like FinSubsequence-like Element of (k *) *
(k *) * is functional non empty FinSequence-membered FinSequenceSet of k *
(k,((k *),D,M)) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,D,M) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[:(k *),(k *):] is Relation-like non empty set
[:[:(k *),(k *):],(k *):] is Relation-like non empty set
bool [:[:(k *),(k *):],(k *):] is non empty cup-closed diff-closed preBoolean set
x is Relation-like [:(k *),(k *):] -defined k * -valued Function-like non empty total quasi_total Function-yielding V50() Element of bool [:[:(k *),(k *):],(k *):]
x "**" ((k *),D,M) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x . (D,M) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[D,M] is set
{D,M} is functional non empty finite V40() countable set
{D} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{D,M},{D}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x . [D,M] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
D is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
M is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
<*D,M,x*> is Relation-like NAT -defined k * -valued Function-like non empty finite 3 -element countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence of k *
(k,<*D,M,x*>) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,D,M) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,(k,D,M),x) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[:(k *),(k *):] is Relation-like non empty set
[:[:(k *),(k *):],(k *):] is Relation-like non empty set
bool [:[:(k *),(k *):],(k *):] is non empty cup-closed diff-closed preBoolean set
i is Relation-like [:(k *),(k *):] -defined k * -valued Function-like non empty total quasi_total Function-yielding V50() Element of bool [:[:(k *),(k *):],(k *):]
i "**" <*D,M,x*> is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
i . (D,M) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[D,M] is set
{D,M} is functional non empty finite V40() countable set
{D} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{D,M},{D}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
i . [D,M] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
i . ((i . (D,M)),x) is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
[(i . (D,M)),x] is set
{(i . (D,M)),x} is functional non empty finite V40() countable set
{(i . (D,M))} is functional non empty trivial finite V40() 1 -element with_common_domain countable set
{{(i . (D,M)),x},{(i . (D,M))}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
i . [(i . (D,M)),x] is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
(k,(i . (D,M)),x) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
k is set
k * is functional non empty FinSequence-membered FinSequenceSet of k
D is Relation-like NAT -defined k * -valued Function-like finite countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence of k *
M is Relation-like NAT -defined k * -valued Function-like finite countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence of k *
(k,D) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,M) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
x is Relation-like NAT -defined k * -valued Function-like finite countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence of k *
D ^ x is Relation-like NAT -defined k * -valued Function-like finite countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence of k *
(k,x) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
(k,(k,D),(k,x)) is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like Element of k *
F1() is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
D is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
D is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
D + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
k + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
Seg (k + 1) is non empty finite k + 1 -element countable Element of bool NAT
k is set
{} |_2 k is Relation-like set
[:k,k:] is Relation-like set
{} /\ [:k,k:] is Relation-like NAT -defined RAT -valued finite countable complex-valued ext-real-valued real-valued natural-valued set
k is set
Fin k is non empty cup-closed diff-closed preBoolean set
bool (Fin k) is non empty cup-closed diff-closed preBoolean set
k is non empty set
Fin k is non empty cup-closed diff-closed preBoolean set
bool (Fin k) is non empty cup-closed diff-closed preBoolean set
the Element of k is Element of k
{ the Element of k} is non empty trivial finite 1 -element countable Element of bool k
bool k is non empty cup-closed diff-closed preBoolean set
{{ the Element of k}} is non empty trivial finite V40() 1 -element countable with_non-empty_elements non empty-membered Element of bool (bool k)
bool (bool k) is non empty cup-closed diff-closed preBoolean set
M is Element of bool (Fin k)
k is non empty set
Fin k is non empty cup-closed diff-closed preBoolean set
bool (Fin k) is non empty cup-closed diff-closed preBoolean set
D is non empty with_non-empty_elements non empty-membered Element of bool (Fin k)
the non empty Element of D is non empty Element of D
k is non empty set
Fin k is non empty cup-closed diff-closed preBoolean set
bool (Fin k) is non empty cup-closed diff-closed preBoolean set
the Element of k is Element of k
{ the Element of k} is non empty trivial finite 1 -element countable Element of bool k
bool k is non empty cup-closed diff-closed preBoolean set
{{ the Element of k}} is non empty trivial finite V40() 1 -element countable with_non-empty_elements non empty-membered Element of bool (bool k)
bool (bool k) is non empty cup-closed diff-closed preBoolean set
M is Element of bool (Fin k)
k is non empty set
[:k,k:] is Relation-like non empty set
bool [:k,k:] is non empty cup-closed diff-closed preBoolean set
bool k is non empty cup-closed diff-closed preBoolean set
D is Relation-like k -defined k -valued total quasi_total reflexive antisymmetric transitive Element of bool [:k,k:]
M is Element of bool k
D |_2 M is Relation-like set
[:M,M:] is Relation-like set
D /\ [:M,M:] is Relation-like k -defined k -valued set
bool [:M,M:] is non empty cup-closed diff-closed preBoolean set
F1() is set
bool F1() is non empty cup-closed diff-closed preBoolean set
F2() is Element of bool F1()
{} F1() 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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of bool F1()
bool F2() is non empty cup-closed diff-closed preBoolean Element of bool (bool F2())
bool F2() is non empty cup-closed diff-closed preBoolean set
bool (bool F2()) is non empty cup-closed diff-closed preBoolean set
k is set
D is set
D is Element of bool (bool F2())
M is set
F2() \ M is Element of bool F1()
the Element of F2() \ M is Element of F2() \ M
{ the Element of F2() \ M} is non empty trivial finite 1 -element countable set
M \/ { the Element of F2() \ M} is non empty set
i is set
x is set
k is non empty set
Fin k is non empty cup-closed diff-closed preBoolean set
bool (Fin k) is non empty cup-closed diff-closed preBoolean set
D is non empty non empty-membered Element of bool (Fin k)
M is non empty set
x is Element of D
k is finite countable set
D is finite countable set
card k is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
card D is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
bool D is non empty cup-closed diff-closed preBoolean finite V40() countable set
M is finite countable Element of bool D
incl M is Relation-like M -defined D -valued M -valued Function-like one-to-one total quasi_total finite countable reflexive symmetric antisymmetric transitive Element of bool [:M,D:]
[:M,D:] is Relation-like finite countable set
bool [:M,D:] is non empty cup-closed diff-closed preBoolean finite V40() countable set
rng (incl M) is finite countable Element of bool D
k is set
bool k is non empty cup-closed diff-closed preBoolean set
[:k,k:] is Relation-like set
bool [:k,k:] is non empty cup-closed diff-closed preBoolean set
M is Relation-like k -defined k -valued total quasi_total reflexive antisymmetric transitive Element of bool [:k,k:]
D is finite countable Element of bool k
(k) is Relation-like non-empty empty-yielding NAT -defined k -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of k *
k * is functional non empty FinSequence-membered FinSequenceSet of k
rng (k) 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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V72() V73() V74() V77() with_non-empty_elements Element of bool k
dom (k) 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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V77() Element of bool NAT
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
i is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
(k) /. x is Element of k
(k) /. i is Element of k
[((k) /. x),((k) /. i)] is set
{((k) /. x),((k) /. i)} is non empty finite countable set
{((k) /. x)} is non empty trivial finite 1 -element countable set
{{((k) /. x),((k) /. i)},{((k) /. x)}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x is non empty set
bool x is non empty cup-closed diff-closed preBoolean set
[:x,x:] is Relation-like non empty set
bool [:x,x:] is non empty cup-closed diff-closed preBoolean set
i is non empty finite countable Element of bool x
Fg is Relation-like x -defined x -valued total quasi_total reflexive antisymmetric transitive Element of bool [:x,x:]
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,a1 & not b1 = a1 ) } is set
db is Element of i
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,db & not b1 = db ) } is set
card H2(db) is epsilon-transitive epsilon-connected ordinal cardinal set
(card H2(db)) +^ 1 is epsilon-transitive epsilon-connected ordinal set
{ H1(b1) where b1 is Element of i : S1[b1] } is set
k1 is finite countable set
card k1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
k2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
k2 +^ 1 is epsilon-transitive epsilon-connected ordinal set
k2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
[:i,NAT:] is Relation-like non empty non trivial non finite non empty-membered set
bool [:i,NAT:] is non empty non trivial cup-closed diff-closed preBoolean non finite non empty-membered set
db is Relation-like i -defined NAT -valued Function-like non empty total quasi_total finite countable complex-valued ext-real-valued real-valued natural-valued Element of bool [:i,NAT:]
k1 is Element of i
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,k1 & not b1 = k1 ) } is set
k2 is Element of i
k1 is Element of i
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,k1 & not b1 = k1 ) } is set
k2 is set
i1 is Element of i
rng db is non empty finite countable V72() V73() V74() V77() Element of bool NAT
card i is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
Seg (card i) is non empty finite card i -element countable Element of bool NAT
k1 is set
dom db is non empty finite countable Element of bool i
bool i is non empty cup-closed diff-closed preBoolean finite V40() countable set
k2 is set
db . k2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
j1 is Element of i
{ H1(b1) where b1 is Element of i : S1[b1] } is set
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,j1 & not b1 = j1 ) } is set
dbi1 is finite countable set
card dbi1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
(card dbi1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
(card dbi1) +^ 1 is epsilon-transitive epsilon-connected ordinal set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
i1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
[:i,(Seg (card i)):] is Relation-like non empty finite countable set
bool [:i,(Seg (card i)):] is non empty cup-closed diff-closed preBoolean finite V40() countable set
M |_2 D is Relation-like set
[:D,D:] is Relation-like finite countable set
M /\ [:D,D:] is Relation-like k -defined k -valued finite countable set
(x,Fg,i) is Relation-like i -defined i -valued total quasi_total finite countable reflexive antisymmetric transitive Element of bool [:i,i:]
[:i,i:] is Relation-like non empty finite countable set
bool [:i,i:] is non empty cup-closed diff-closed preBoolean finite V40() countable set
Fg /\ [:i,i:] is Relation-like x -defined x -valued finite countable set
field (x,Fg,i) is finite countable set
dom (x,Fg,i) is finite countable set
rng (x,Fg,i) is finite countable set
(dom (x,Fg,i)) \/ (rng (x,Fg,i)) is finite countable set
k2 is set
i1 is set
db . k2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
db . i1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
dbi1 is Element of i
{ H1(b1) where b1 is Element of i : S1[b1] } is set
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,dbi1 & not b1 = dbi1 ) } is set
j1 is Element of i
{ H1(b1) where b1 is Element of i : S2[b1] } is set
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,j1 & not b1 = j1 ) } is set
b12 is Element of i
b119 is Element of i
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,b12 & not b1 = b12 ) } is set
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,b119 & not b1 = b119 ) } is set
[b12,b119] is Element of [:i,i:]
{b12,b119} is non empty finite countable set
{b12} is non empty trivial finite 1 -element countable set
{{b12,b119},{b12}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
b129 is set
b111 is Element of D
[b111,b12] is set
{b111,b12} is non empty finite countable set
{b111} is non empty trivial finite 1 -element countable set
{{b111,b12},{b111}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
[b111,b119] is set
{b111,b119} is non empty finite countable set
{{b111,b119},{b111}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
db . dbi1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
ddbi11 is finite countable set
card ddbi11 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
(card ddbi11) +^ 1 is epsilon-transitive epsilon-connected ordinal set
(card ddbi11) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
b11 is finite countable set
card b11 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
(card b11) +^ 1 is epsilon-transitive epsilon-connected ordinal set
(card b11) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
[dbi1,j1] is Element of [:i,i:]
{dbi1,j1} is non empty finite countable set
{dbi1} is non empty trivial finite 1 -element countable set
{{dbi1,j1},{dbi1}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
[j1,dbi1] is Element of [:i,i:]
{j1,dbi1} is non empty finite countable set
{j1} is non empty trivial finite 1 -element countable set
{{j1,dbi1},{j1}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
b12 is Element of i
b119 is Element of i
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,b119 & not b1 = b119 ) } is set
[b12,b119] is Element of [:i,i:]
{b12,b119} is non empty finite countable set
{b12} is non empty trivial finite 1 -element countable set
{{b12,b119},{b12}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
k1 is Relation-like i -defined Seg (card i) -valued Function-like non empty total quasi_total finite countable Element of bool [:i,(Seg (card i)):]
i1 is Element of i
db . i1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
k2 is Element of i
db . k2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
{ H1(b1) where b1 is Element of i : S1[b1] } is set
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,k2 & not b1 = k2 ) } is set
{ H1(b1) where b1 is Element of i : S2[b1] } is set
{ H1(b1) where b1 is Element of i : ( b1 <=_ Fg,i1 & not b1 = i1 ) } is set
j1 is finite countable set
card j1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
(card j1) +^ 1 is epsilon-transitive epsilon-connected ordinal set
(card j1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
dbi1 is finite countable set
card dbi1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
(card dbi1) +^ 1 is epsilon-transitive epsilon-connected ordinal set
(card dbi1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
((card dbi1) + 1) - 1 is V55() real ext-real Element of REAL
((card j1) + 1) - 1 is V55() real ext-real Element of REAL
card (card dbi1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
card (card j1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
b11 is epsilon-transitive epsilon-connected ordinal cardinal set
ddbi11 is epsilon-transitive epsilon-connected ordinal cardinal set
dbi1 \ j1 is finite countable Element of bool dbi1
bool dbi1 is non empty cup-closed diff-closed preBoolean finite V40() countable set
b12 is set
b119 is Element of i
[b119,i1] is Element of [:i,i:]
{b119,i1} is non empty finite countable set
{b119} is non empty trivial finite 1 -element countable set
{{b119,i1},{b119}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
b129 is Element of i
[b119,k2] is Element of [:i,i:]
{b119,k2} is non empty finite countable set
{{b119,k2},{b119}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
b129 is Element of i
[k2,b119] is Element of [:i,i:]
{k2,b119} is non empty finite countable set
{k2} is non empty trivial finite 1 -element countable set
{{k2,b119},{k2}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
[k2,i1] is Element of [:i,i:]
{k2,i1} is non empty finite countable set
{{k2,i1},{k2}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
b129 is Element of i
card (Seg (card i)) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
rng k1 is non empty finite countable Element of bool (Seg (card i))
bool (Seg (card i)) is non empty cup-closed diff-closed preBoolean finite V40() countable set
k1 " is Relation-like Function-like set
dom (k1 ") is set
dom k1 is non empty finite countable Element of bool i
bool i is non empty cup-closed diff-closed preBoolean finite V40() countable set
k2 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
rng k2 is finite countable set
i1 is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of k
rng i1 is finite countable Element of bool k
dom i1 is finite countable V77() Element of bool NAT
j1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
dbi1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
i1 /. j1 is Element of k
i1 /. dbi1 is Element of k
[(i1 /. j1),(i1 /. dbi1)] is set
{(i1 /. j1),(i1 /. dbi1)} is non empty finite countable set
{(i1 /. j1)} is non empty trivial finite 1 -element countable set
{{(i1 /. j1),(i1 /. dbi1)},{(i1 /. j1)}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
i1 . j1 is set
ddbi11 is Element of i
db . ddbi11 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
i1 . dbi1 is set
b11 is Element of i
db . b11 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
[ddbi11,b11] is Element of [:i,i:]
{ddbi11,b11} is non empty finite countable set
{ddbi11} is non empty trivial finite 1 -element countable set
{{ddbi11,b11},{ddbi11}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
x is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of k
rng x is finite countable Element of bool k
dom x is finite countable V77() Element of bool NAT
i is Relation-like NAT -defined k -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of k
rng i is finite countable Element of bool k
dom i is finite countable V77() Element of bool NAT
Fg is non empty set
bool Fg is non empty cup-closed diff-closed preBoolean set
db is non empty finite countable Element of bool Fg
(db) is Relation-like non-empty empty-yielding NAT -defined db -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued Element of db *
db * is functional non empty FinSequence-membered FinSequenceSet of db
j1 is Relation-like NAT -defined db -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of db
dom j1 is finite countable V77() Element of bool NAT
rng j1 is finite countable Element of bool db
bool db is non empty cup-closed diff-closed preBoolean finite V40() countable set
dbi1 is Element of db
(db,dbi1) is Relation-like NAT -defined db -valued Function-like constant non empty trivial finite 1 -element countable FinSequence-like FinSubsequence-like Element of db *
j1 ^ (db,dbi1) is Relation-like NAT -defined Fg -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like M26(Fg,db)
dom (j1 ^ (db,dbi1)) is non empty finite countable V77() Element of bool NAT
rng (j1 ^ (db,dbi1)) is non empty finite countable Element of bool db
ddbi11 is Relation-like NAT -defined db -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of db
rng ddbi11 is finite countable Element of bool db
dom ddbi11 is finite countable V77() Element of bool NAT
rng (j1 ^ (db,dbi1)) is non empty finite countable Element of bool Fg
len ddbi11 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
b11 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
b11 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
b12 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
b119 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len b119 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
dom b119 is finite countable V77() Element of bool NAT
b119 is Relation-like NAT -defined Function-like finite countable FinSequence-like FinSubsequence-like set
len b119 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
dom b119 is finite countable V77() Element of bool NAT
dom (db,dbi1) is non empty trivial finite 1 -element countable V77() Element of bool NAT
b129 is Element of db
b111 is Element of db
[b111,b129] is Element of [:db,db:]
[:db,db:] is Relation-like non empty finite countable set
{b111,b129} is non empty finite countable set
{b111} is non empty trivial finite 1 -element countable set
{{b111,b129},{b111}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
b112 is set
(j1 ^ (db,dbi1)) . b112 is set
(j1 ^ (db,dbi1)) /. b112 is Element of db
i2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
len j1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
(len j1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
(j1 ^ (db,dbi1)) . i2 is set
(db,dbi1) . 1 is set
len (j1 ^ (db,dbi1)) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
Seg (len (j1 ^ (db,dbi1))) is non empty finite len (j1 ^ (db,dbi1)) -element countable Element of bool NAT
len (db,dbi1) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
(len j1) + (len (db,dbi1)) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
i2 - i2 is V55() real ext-real Element of REAL
1 - (len (j1 ^ (db,dbi1))) is V55() real ext-real Element of REAL
(j1 ^ (db,dbi1)) . ((len j1) + 1) is set
(j1 ^ (db,dbi1)) . ((len j1) + (len (db,dbi1))) is set
(j1 ^ (db,dbi1)) . (len (j1 ^ (db,dbi1))) is set
(j1 ^ (db,dbi1)) /. (len (j1 ^ (db,dbi1))) is Element of db
b129 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
(len b119) + b129 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
ddbi11 . ((len b119) + b129) is set
(db,dbi1) . b129 is set
{1} is non empty trivial finite V40() 1 -element countable with_non-empty_elements non empty-membered Element of bool NAT
b111 is Element of db
b111 is Element of db
Seg (len ddbi11) is finite len ddbi11 -element countable Element of bool NAT
ddbi11 . (len ddbi11) is set
i2 is Element of db
ddbi11 /. (len ddbi11) is Element of db
field M is set
dom M is set
rng M is set
(dom M) \/ (rng M) is set
{dbi1} is non empty trivial finite 1 -element countable Element of bool db
rng (db,dbi1) is non empty trivial finite 1 -element countable Element of bool db
(rng j1) \/ (rng (db,dbi1)) is non empty finite countable Element of bool db
j2 is set
ddbi11 . j2 is set
dbi2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
b112 is Element of db
[i2,b112] is Element of [:db,db:]
[:db,db:] is Relation-like non empty finite countable set
{i2,b112} is non empty finite countable set
{i2} is non empty trivial finite 1 -element countable set
{{i2,b112},{i2}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
ddbi11 /. dbi2 is Element of db
[b112,i2] is Element of [:db,db:]
{b112,i2} is non empty finite countable set
{b112} is non empty trivial finite 1 -element countable set
{{b112,i2},{b112}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
b12 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
b129 is set
rng b119 is finite countable set
b111 is set
b119 . b111 is set
Seg (len b119) is finite len b119 -element countable Element of bool NAT
b112 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
ddbi11 . b112 is set
Seg (b12 + 1) is non empty finite b12 + 1 -element b12 + 1 -element countable Element of bool NAT
b12 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
len (db,dbi1) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
(len b119) + (len (db,dbi1)) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
Seg ((len b119) + (len (db,dbi1))) is non empty finite (len b119) + (len (db,dbi1)) -element countable Element of bool NAT
b119 ^ (db,dbi1) is Relation-like NAT -defined Function-like non empty finite countable FinSequence-like FinSubsequence-like set
len j1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
(len j1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
(len j1) + (len (db,dbi1)) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
len (j1 ^ (db,dbi1)) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
Seg (len (j1 ^ (db,dbi1))) is non empty finite len (j1 ^ (db,dbi1)) -element countable Element of bool NAT
b111 is set
j1 . b111 is set
Seg (len j1) is finite len j1 -element countable Element of bool NAT
b112 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
(j1 ^ (db,dbi1)) . b112 is set
(j1 ^ (db,dbi1)) /. b112 is Element of db
(j1 ^ (db,dbi1)) . ((len j1) + 1) is set
(j1 ^ (db,dbi1)) /. ((len j1) + 1) is Element of db
{dbi1} is non empty trivial finite 1 -element countable Element of bool db
(rng j1) \/ {dbi1} is non empty finite countable Element of bool db
((rng j1) \/ {dbi1}) \ {dbi1} is finite countable Element of bool db
b111 is set
rng (db,dbi1) is non empty trivial finite 1 -element countable Element of bool db
(rng j1) \/ (rng (db,dbi1)) is non empty finite countable Element of bool db
(rng (j1 ^ (db,dbi1))) \ {dbi1} is finite countable Element of bool Fg
b129 is Relation-like NAT -defined db -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of db
rng b129 is finite countable Element of bool db
dom b129 is finite countable V77() Element of bool NAT
len b129 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
(len b129) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
(len b129) + (len (db,dbi1)) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
b129 ^ (db,dbi1) is Relation-like NAT -defined Fg -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like M26(Fg,db)
len (b129 ^ (db,dbi1)) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable V55() real ext-real positive non negative Element of NAT
Seg (len (b129 ^ (db,dbi1))) is non empty finite len (b129 ^ (db,dbi1)) -element countable Element of bool NAT
dom (b129 ^ (db,dbi1)) is non empty finite countable V77() Element of bool NAT
b111 is set
b129 . b111 is set
Seg (len b129) is finite len b129 -element countable Element of bool NAT
b112 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative Element of NAT
ddbi11 . b112 is set
ddbi11 /. b112 is Element of db
ddbi11 . ((len b129) + 1) is set
ddbi11 /. ((len b129) + 1) is Element of db
(rng b129) \/ {dbi1} is non empty finite countable Element of bool db
((rng b129) \/ {dbi1}) \ {dbi1} is finite countable Element of bool db
b111 is set
b129 ^ (db,dbi1) is Relation-like NAT -defined Fg -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like M26(Fg,db)
rng (b129 ^ (db,dbi1)) is non empty finite countable Element of bool Fg
(rng b129) \/ (rng (db,dbi1)) is non empty finite countable Element of bool db
b111 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
b112 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
b129 /. b111 is Element of db
b129 /. b112 is Element of db
[(b129 /. b111),(b129 /. b112)] is Element of [:db,db:]
[:db,db:] is Relation-like non empty finite countable set
{(b129 /. b111),(b129 /. b112)} is non empty finite countable set
{(b129 /. b111)} is non empty trivial finite 1 -element countable set
{{(b129 /. b111),(b129 /. b112)},{(b129 /. b111)}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
b129 . b112 is set
ddbi11 . b112 is set
ddbi11 /. b112 is Element of db
b129 . b111 is set
ddbi11 . b111 is set
ddbi11 /. b111 is Element of db
b111 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
b112 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
j1 /. b111 is Element of db
j1 /. b112 is Element of db
[(j1 /. b111),(j1 /. b112)] is Element of [:db,db:]
[:db,db:] is Relation-like non empty finite countable set
{(j1 /. b111),(j1 /. b112)} is non empty finite countable set
{(j1 /. b111)} is non empty trivial finite 1 -element countable set
{{(j1 /. b111),(j1 /. b112)},{(j1 /. b111)}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
j1 . b112 is set
(j1 ^ (db,dbi1)) . b112 is set
(j1 ^ (db,dbi1)) /. b112 is Element of db
j1 . b111 is set
(j1 ^ (db,dbi1)) . b111 is set
(j1 ^ (db,dbi1)) /. b111 is Element of db
b111 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
b112 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
j1 /. b111 is Element of db
j1 /. b112 is Element of db
[(j1 /. b111),(j1 /. b112)] is Element of [:db,db:]
[:db,db:] is Relation-like non empty finite countable set
{(j1 /. b111),(j1 /. b112)} is non empty finite countable set
{(j1 /. b111)} is non empty trivial finite 1 -element countable set
{{(j1 /. b111),(j1 /. b112)},{(j1 /. b111)}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
j1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
k2 is Relation-like NAT -defined db -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of db
dom k2 is finite countable V77() Element of bool NAT
dbi1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
k2 /. dbi1 is Element of db
k2 . dbi1 is set
x /. dbi1 is Element of k
k2 /. j1 is Element of db
k2 . j1 is set
x /. j1 is Element of k
[(k2 /. j1),(k2 /. dbi1)] is Element of [:db,db:]
[:db,db:] is Relation-like non empty finite countable set
{(k2 /. j1),(k2 /. dbi1)} is non empty finite countable set
{(k2 /. j1)} is non empty trivial finite 1 -element countable set
{{(k2 /. j1),(k2 /. dbi1)},{(k2 /. j1)}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
j1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
i1 is Relation-like NAT -defined db -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of db
dom i1 is finite countable V77() Element of bool NAT
dbi1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable V55() real ext-real non negative set
i1 /. dbi1 is Element of db
i1 . dbi1 is set
i /. dbi1 is Element of k
i1 /. j1 is Element of db
i1 . j1 is set
i /. j1 is Element of k
[(i1 /. j1),(i1 /. dbi1)] is Element of [:db,db:]
{(i1 /. j1),(i1 /. dbi1)} is non empty finite countable set
{(i1 /. j1)} is non empty trivial finite 1 -element countable set
{{(i1 /. j1),(i1 /. dbi1)},{(i1 /. j1)}} is non empty finite V40() countable with_non-empty_elements non empty-membered set
dom (db) 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 finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V77() Element of bool NAT
rng (db) 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 proper finite finite-yielding V40() cardinal {} -element Cardinal-yielding countable Function-yielding V50() FinSequence-like FinSubsequence-like FinSequence-membered V55() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V72() V73() V74() V77() with_non-empty_elements Element of bool db
bool db is non empty cup-closed diff-closed preBoolean finite V40() countable set
j1 is Relation-like NAT -defined db -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of db
rng j1 is finite countable Element of bool db
dom j1 is finite countable V77() Element of bool NAT
k is set
bool k is non empty cup-closed diff-closed preBoolean set
[:k,k