:: PRE_POLY semantic presentation

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 *

F

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

F

bool F

F

{} F

bool F

bool F

bool (bool F

k is set

D is set

D is Element of bool (bool F

M is set

F

the Element of F

{ the Element of F

M \/ { the Element of F

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:]

{ H

db is Element of i

{ H

card H

(card H

{ H

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

{ H

k2 is Element of i

k1 is Element of i

{ H

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

{ H

{ H

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

{ H

{ H

j1 is Element of i

{ H

{ H

b12 is Element of i

b119 is Element of i

{ H

{ H

[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

{ H

[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

{ H

{ H

{ H

{ H

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