:: PRE_POLY semantic presentation

REAL is set

RAT is set

INT is set

{{},1} is non empty finite V40() countable set

K462() is set

K463() is Element of bool K462()

is Relation-like non empty non trivial non finite non empty-membered set

K576() is set

Seg 1 is non empty trivial finite 1 -element countable Element of bool NAT

Seg 2 is non empty finite 2 -element countable Element of bool NAT

K430(()) is V55() real ext-real Element of REAL

k is set

k is set

k is set

k is non empty set
D is Element of k

M is Element of k

k is set

k is set

[:(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 *):]

[x,i] is set
{x,i} is functional non empty finite V40() countable set

{{x,i},{x}} is non empty finite V40() countable with_non-empty_elements non empty-membered 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 *):]

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

[db,k1] is set
{db,k1} is functional non empty finite V40() countable set

{{db,k1},{db}} is non empty finite V40() countable with_non-empty_elements non empty-membered set

k is set

[:(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 *):]

k is set

[:(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 . ({},x) is set
[{},x] is set

D . (x,{}) is set
[x,{}] is set

k is set

[:(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 *):]

[Fg,db] is set
{Fg,db} is functional non empty finite V40() countable set

{{Fg,db},{Fg}} is non empty finite V40() countable with_non-empty_elements non empty-membered set

[i,(x . (Fg,db))] is set
{i,(x . (Fg,db))} is functional non empty finite V40() countable set

{{i,(x . (Fg,db))},{i}} is non empty finite V40() countable with_non-empty_elements non empty-membered set

[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)),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 . ({},Fg) is set
[{},Fg] is set
{{},Fg} is functional non empty finite V40() countable set

x . (Fg,{}) is set
[Fg,{}] is set
{Fg,{}} is functional non empty finite V40() countable set

{{Fg,{}},{Fg}} is non empty finite V40() countable with_non-empty_elements non empty-membered set

[(x "**" D),(x "**" M)] is set
{(x "**" D),(x "**" M)} is functional non empty finite V40() countable set

{{(x "**" D),(x "**" M)},{(x "**" D)}} is non empty finite V40() countable with_non-empty_elements non empty-membered set

k is set

[:(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 *):]

[D,M] is set
{D,M} is functional non empty finite V40() countable set

{{D,M},{D}} is non empty finite V40() countable with_non-empty_elements non empty-membered set

k is set

[:(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 *):]

[D,M] is set
{D,M} is functional non empty finite V40() countable set

{{D,M},{D}} is non empty finite V40() countable with_non-empty_elements non empty-membered set

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

k is set

Seg (k + 1) is non empty finite k + 1 -element countable Element of bool NAT
k is set

[:k,k:] is Relation-like set

k is set

bool (Fin k) is non empty cup-closed diff-closed preBoolean set
k is non empty 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

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

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

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

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

M is Element of bool k

[:M,M:] is Relation-like set

F1() is set
bool F1() is non empty cup-closed diff-closed preBoolean set
F2() is 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

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

rng (incl M) is finite countable Element of bool D
k is set

[:k,k:] is Relation-like 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

[:x,x:] is Relation-like non empty set

i is non empty finite countable Element of bool 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)) +^ 1 is epsilon-transitive epsilon-connected ordinal set
{ H1(b1) where b1 is Element of i : S1[b1] } is set

[:i,NAT:] is Relation-like non empty non trivial non finite non empty-membered set

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

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

k2 is 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

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

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

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

ddbi11 is finite countable set

(card ddbi11) +^ 1 is epsilon-transitive epsilon-connected ordinal set

b11 is finite countable set

[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

i1 is Element of i

k2 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,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

dbi1 is finite countable set

((card dbi1) + 1) - 1 is V55() real ext-real Element of REAL
((card j1) + 1) - 1 is V55() real ext-real Element of REAL

dbi1 \ j1 is finite countable Element of bool dbi1

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

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

dom (k1 ") is set
dom k1 is non empty finite countable Element of bool i

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

i1 . dbi1 is set
b11 is Element of i

[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

Fg is non empty set

db is non empty finite countable Element of bool Fg

rng j1 is finite countable Element of bool db

dbi1 is 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

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

dom b119 is finite countable V77() Element of bool 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

(j1 ^ (db,dbi1)) . i2 is set
(db,dbi1) . 1 is set

Seg (len (j1 ^ (db,dbi1))) is non empty finite len (j1 ^ (db,dbi1)) -element countable Element of bool 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

ddbi11 . ((len b119) + b129) is set
(db,dbi1) . b129 is set

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

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

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

ddbi11 . b112 is set
Seg (b12 + 1) is non empty finite b12 + 1 -element b12 + 1 -element countable Element of bool NAT

Seg ((len b119) + (len (db,dbi1))) is non empty finite (len b119) + (len (db,dbi1)) -element countable Element of bool 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

(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

rng b129 is finite countable Element of bool db
dom b129 is finite countable V77() Element of bool NAT

b129 ^ (db,dbi1) is Relation-like NAT -defined Fg -valued Function-like non empty finite countable FinSequence-like FinSubsequence-like M26(Fg,db)

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

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

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

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

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

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

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

rng j1 is finite countable Element of bool db

k is set

[:k,k