:: FINSOP_1 semantic presentation

REAL is set

NAT is non empty V35() V36() V37() V43() V48() V49() Element of K19(REAL)

K19(REAL) is set

{} is Function-like functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-membered set

the Function-like functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-membered set is Function-like functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-membered set

NAT is non empty V35() V36() V37() V43() V48() V49() set

K19(NAT) is V43() set

K19(NAT) is V43() set

1 is non empty ext-real positive non negative V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

2 is non empty ext-real positive non negative V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

3 is non empty ext-real positive non negative V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

0 is Function-like functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-membered Element of NAT

Seg 1 is non empty V12() V43() V50(1) Element of K19(NAT)

{1} is non empty V12() V50(1) set

Seg 2 is non empty V43() V50(2) Element of K19(NAT)

{1,2} is non empty set

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

the_unity_wrt g is Element of D

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

F . 1 is set

k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

k + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l . 1 is set

Seg k is V43() V50(k) Element of K19(NAT)

l | (Seg k) is Relation-like NAT -defined D -valued Function-like FinSubsequence-like Element of K19(K20(NAT,D))

l is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

NAT --> (l . 1) is Relation-like NAT -defined {(l . 1)} -valued Function-like non empty total quasi_total Element of K19(K20(NAT,{(l . 1)}))

{(l . 1)} is non empty V12() V50(1) set

K20(NAT,{(l . 1)}) is V43() set

K19(K20(NAT,{(l . 1)})) is V43() set

rng (NAT --> (l . 1)) is set

k is set

dom (NAT --> (l . 1)) is Element of K19(NAT)

d is set

(NAT --> (l . 1)) . d is set

dom l is Element of K19(NAT)

rng l is set

dom (NAT --> (l . 1)) is Element of K19(NAT)

k is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

k . 1 is Element of D

f is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

f . 1 is Element of D

gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

f . (gg + 1) is Element of D

f . gg is Element of D

l . (gg + 1) is set

g . ((f . gg),(l . (gg + 1))) is set

d is Element of D

f . (len l) is Element of D

dom l is Element of K19(NAT)

l . (len l) is set

rng l is set

dom l is Element of K19(NAT)

l . 1 is set

f is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

f . 1 is Element of D

d is Element of D

f . (len l) is Element of D

g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

k is Element of D

g . (d,k) is Element of D

gg is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

gg . g is Element of D

d is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

d . 1 is Element of D

d1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d1 + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d . (d1 + 1) is Element of D

d . d1 is Element of D

l . (d1 + 1) is set

g . ((d . d1),(l . (d1 + 1))) is set

f . (d1 + 1) is Element of D

f . d1 is Element of D

l . (d1 + 1) is set

g . ((f . d1),(l . (d1 + 1))) is set

g . ((f . d1),(l . (d1 + 1))) is set

h is Element of D

d . (len l) is Element of D

k is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

k . 1 is Element of D

g is Element of D

k . (len l) is Element of D

k is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

k . 1 is set

k is Element of D

l is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

l . 1 is Element of D

l is Element of D

l . (len F) is Element of D

k is Element of D

l is Element of D

l is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

l . 1 is Element of D

l . (len F) is Element of D

g is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

g . 1 is Element of D

g . (len F) is Element of D

k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l . k is Element of D

g . k is Element of D

k + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l . (k + 1) is Element of D

g . (k + 1) is Element of D

F . (k + 1) is set

g . ((l . k),(F . (k + 1))) is set

l . 0 is Element of D

g . 0 is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

F . 1 is set

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,g) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

l . 1 is Element of D

g . 1 is set

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

F is Element of D

l . (len g) is Element of D

(D,g,k) is Element of D

D is non empty set

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

F is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

F +* g is Relation-like Function-like set

dom F is Element of K19(NAT)

F +* g is Relation-like NAT -defined D -valued Function-like Element of K19(K20(NAT,D))

dom (F +* g) is Element of K19(NAT)

dom g is Element of K19(NAT)

(dom F) \/ (dom g) is Element of K19(NAT)

D is Relation-like NAT -defined Function-like V43() FinSequence-like FinSubsequence-like set

dom D is set

Fin NAT is preBoolean set

dom D is Element of K19(NAT)

len D is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

Seg (len D) is V43() V50( len D) Element of K19(NAT)

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(F) is Element of Fin NAT

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,g) is Element of D

the_unity_wrt g is Element of D

NAT --> (the_unity_wrt g) is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

(D,(NAT --> (the_unity_wrt g)),F) is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

g $$ ((F),(D,(NAT --> (the_unity_wrt g)),F)) is Element of D

dom F is Element of K19(NAT)

Seg (len F) is V43() V50( len F) Element of K19(NAT)

K20((Fin NAT),D) is set

K19(K20((Fin NAT),D)) is set

l is Relation-like Fin NAT -defined D -valued Function-like total quasi_total Element of K19(K20((Fin NAT),D))

l . (F) is set

l . {} is set

F . 1 is set

g is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

g . 1 is Element of D

g . (len F) is Element of D

k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g . k is Element of D

Seg k is V43() V50(k) Element of K19(NAT)

l . (Seg k) is set

k + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g . (k + 1) is Element of D

Seg (k + 1) is V43() V50(k + 1) Element of K19(NAT)

l . (Seg (k + 1)) is set

(D,(NAT --> (the_unity_wrt g)),F) . 1 is Element of D

F . (k + 1) is set

g . ((g . k),(F . (k + 1))) is set

(F) \ (Seg k) is Element of K19((F))

K19((F)) is set

{(k + 1)} is non empty V12() V50(1) set

(Seg k) \/ {(k + 1)} is non empty set

l . ((Seg k) \/ {(k + 1)}) is set

d is Element of Fin NAT

l . d is set

(D,(NAT --> (the_unity_wrt g)),F) . (k + 1) is Element of D

g . ((l . d),((D,(NAT --> (the_unity_wrt g)),F) . (k + 1))) is set

g . 0 is Element of D

Seg 0 is Function-like functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( 0 ) V50( {} ) FinSequence-membered Element of K19(NAT)

l . (Seg 0) is set

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(F) is Element of Fin NAT

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,g) is Element of D

the_unity_wrt g is Element of D

NAT --> (the_unity_wrt g) is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

(D,(NAT --> (the_unity_wrt g)),F) is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

g $$ ((F),(D,(NAT --> (the_unity_wrt g)),F)) is Element of D

dom F is Element of K19(NAT)

{}. NAT is Function-like functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-membered Element of Fin NAT

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(F) is Element of Fin NAT

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,g) is Element of D

the_unity_wrt g is Element of D

NAT --> (the_unity_wrt g) is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

(D,(NAT --> (the_unity_wrt g)),F) is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

g $$ ((F),(D,(NAT --> (the_unity_wrt g)),F)) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

<*> D is Relation-like NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D

F is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(<*> D),F) is Element of D

the_unity_wrt F is Element of D

len (<*> D) is Function-like functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-membered Element of NAT

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

<*F*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,<*F*>,g) is Element of D

len <*F*> is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

<*F*> . 1 is set

k is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

k . 1 is Element of D

k . (len <*F*>) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

<*F*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g ^ <*F*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(g ^ <*F*>),k) is Element of D

(D,g,k) is Element of D

k . ((D,g,k),F) is Element of D

(len g) + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(g ^ <*F*>) . ((len g) + 1) is set

len (g ^ <*F*>) is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

len <*F*> is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(len g) + (len <*F*>) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

(g ^ <*F*>) . 1 is set

l is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

l . 1 is Element of D

l . (len (g ^ <*F*>)) is Element of D

g . 1 is set

g is Relation-like NAT -defined D -valued Function-like non empty total quasi_total Element of K19(K20(NAT,D))

g . 1 is Element of D

g . (len g) is Element of D

k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g . k is Element of D

l . k is Element of D

k + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g . (k + 1) is Element of D

l . (k + 1) is Element of D

dom g is Element of K19(NAT)

(g ^ <*F*>) . (k + 1) is set

k . ((l . k),((g ^ <*F*>) . (k + 1))) is set

dom g is Element of K19(NAT)

0 + 1 is non empty ext-real positive non negative V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g . (k + 1) is set

k . ((g . k),(g . (k + 1))) is set

g . 0 is Element of D

l . 0 is Element of D

l . (len g) is Element of D

k . ((l . (len g)),((g ^ <*F*>) . ((len g) + 1))) is set

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

<*F*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g ^ <*F*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(g ^ <*F*>),k) is Element of D

(D,g,k) is Element of D

k . ((D,g,k),F) is Element of D

<*> D is Relation-like NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D

(D,<*F*>,k) is Element of D

the_unity_wrt k is Element of D

k . ((the_unity_wrt k),F) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

<*F*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g ^ <*F*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(g ^ <*F*>),k) is Element of D

(D,g,k) is Element of D

k . ((D,g,k),F) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

F ^ g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(F ^ g),k) is Element of D

(D,F,k) is Element of D

(D,g,k) is Element of D

k . ((D,F,k),(D,g,k)) is Element of D

l is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l is Element of D

<*l*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

l ^ <*l*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

len (l ^ <*l*>) is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g ^ (l ^ <*l*>) is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(g ^ (l ^ <*l*>)),k) is Element of D

(D,g,k) is Element of D

(D,(l ^ <*l*>),k) is Element of D

k . ((D,g,k),(D,(l ^ <*l*>),k)) is Element of D

g ^ l is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len (g ^ l) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(len g) + (len l) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(g ^ l) ^ <*l*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

(D,((g ^ l) ^ <*l*>),k) is Element of D

(D,(g ^ l),k) is Element of D

k . ((D,(g ^ l),k),l) is Element of D

(D,l,k) is Element of D

k . ((D,g,k),(D,l,k)) is Element of D

k . ((k . ((D,g,k),(D,l,k))),l) is Element of D

k . ((D,l,k),l) is Element of D

k . ((D,g,k),(k . ((D,l,k),l))) is Element of D

g ^ <*l*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

(D,(g ^ <*l*>),k) is Element of D

k . ((D,g,k),l) is Element of D

(D,<*l*>,k) is Element of D

k . ((D,g,k),(D,<*l*>,k)) is Element of D

<*> D is Relation-like NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D

len (<*> D) is Function-like functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-membered Element of NAT

l is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l ^ (<*> D) is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

l is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(l ^ (<*> D)),l) is Element of D

(D,l,l) is Element of D

(D,(<*> D),l) is Element of D

l . ((D,l,l),(D,(<*> D),l)) is Element of D

the_unity_wrt l is Element of D

l . ((D,l,l),(the_unity_wrt l)) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

<*F*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

<*F*> ^ g is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(<*F*> ^ g),k) is Element of D

(D,g,k) is Element of D

k . (F,(D,g,k)) is Element of D

len <*F*> is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(D,<*F*>,k) is Element of D

k . ((D,<*F*>,k),(D,g,k)) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

dom F is Element of K19(NAT)

K20((dom F),(dom F)) is set

K19(K20((dom F),(dom F))) is set

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom g is Element of K19(NAT)

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,k) is Element of D

(D,g,k) is Element of D

l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom l is Element of K19(NAT)

K20((dom l),(dom l)) is set

K19(K20((dom l),(dom l))) is set

(D,l,k) is Element of D

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom g is Element of K19(NAT)

(D,g,k) is Element of D

Seg l is V43() V50(l) Element of K19(NAT)

g | (Seg l) is Relation-like NAT -defined D -valued Function-like FinSubsequence-like Element of K19(K20(NAT,D))

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

d is Relation-like dom l -defined dom l -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom l),(dom l)))

Seg (l + 1) is V43() V50(l + 1) Element of K19(NAT)

rng d is set

f is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom d is Element of K19((dom l))

K19((dom l)) is set

d . f is set

rng g is set

d . (l + 1) is set

g . (l + 1) is set

f is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

h is ext-real V34() V35() V36() V37() V41() V42() V43() V48() set

f + h is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d is ext-real V34() V35() V36() V37() V41() V42() V43() V48() set

1 + d is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d2 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

Seg d2 is V43() V50(d2) Element of K19(NAT)

q2 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() set

f + q2 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l . (f + q2) is set

q2 is Relation-like NAT -defined Function-like V43() FinSequence-like FinSubsequence-like set

dom q2 is Element of K19(NAT)

rng q2 is set

q2 is set

(q2) is Element of Fin NAT

q1 is set

q2 . q1 is set

gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

f + gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

Seg (len l) is V43() V50( len l) Element of K19(NAT)

l . (f + gg) is set

rng l is set

q is Element of D

d1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

Seg d1 is V43() V50(d1) Element of K19(NAT)

l | (Seg d1) is Relation-like NAT -defined D -valued Function-like FinSubsequence-like Element of K19(K20(NAT,D))

q1 is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

dom q1 is Element of K19(NAT)

gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() set

d . gg is set

q is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

q - 1 is ext-real V34() V42() set

gg is ext-real V34() V42() set

gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg - 1 is ext-real V34() V42() set

q is ext-real V34() V42() set

gg is Relation-like NAT -defined Function-like V43() FinSequence-like FinSubsequence-like set

dom gg is Element of K19(NAT)

k is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

dom k is Element of K19(NAT)

gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

q is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d . q is set

d1 + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l + 0 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(d1 + 1) + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d1 + 2 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

1 + l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d1 + d2 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

1 + (d1 + d2) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

rng gg is set

q is set

(gg) is Element of Fin NAT

gg is set

gg . gg is set

gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d . gg is set

gg . gg is set

gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d . gg is set

i is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

i - 1 is ext-real V34() V42() set

j is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(l + 1) - 1 is ext-real V34() V42() set

(d1 + 2) - 1 is ext-real V34() V42() set

gg . gg is set

gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d . gg is set

len q1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

q is ext-real V34() V35() V36() V37() V41() V42() V43() V48() set

q2 is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

dom q2 is Element of K19(NAT)

gg is Element of D

<*gg*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

q1 ^ <*gg*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

len (q1 ^ <*gg*>) is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

len <*gg*> is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d1 + (len <*gg*>) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(len (q1 ^ <*gg*>)) + q is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l . ((len (q1 ^ <*gg*>)) + q) is set

q2 . q is set

q1 ^ q2 is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len q2 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

len (q1 ^ q2) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom (q1 ^ q2) is Element of K19(NAT)

K20((dom (q1 ^ q2)),(dom (q1 ^ q2))) is set

K19(K20((dom (q1 ^ q2)),(dom (q1 ^ q2)))) is set

len k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like total quasi_total Element of K19(K20((dom (q1 ^ q2)),(dom (q1 ^ q2))))

rng gg is set

gg is set

j is set

d . j is set

j1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom gg is Element of K19((dom (q1 ^ q2)))

K19((dom (q1 ^ q2))) is set

d . j1 is set

gg . j1 is set

d . j1 is set

i is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

i + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

a is set

d . a is set

(Seg (l + 1)) \ (Seg l) is Element of K19(NAT)

{(l + 1)} is non empty V12() V50(1) set

gg . a is set

(i + 1) - 1 is ext-real V34() V42() set

d . j1 is set

j1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom gg is Element of K19((dom (q1 ^ q2)))

K19((dom (q1 ^ q2))) is set

i is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

i + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

a is set

d . a is set

(Seg (l + 1)) \ (Seg l) is Element of K19(NAT)

{(l + 1)} is non empty V12() V50(1) set

i + 0 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg . a is set

(i + 1) - 1 is ext-real V34() V42() set

j1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom gg is Element of K19((dom (q1 ^ q2)))

K19((dom (q1 ^ q2))) is set

l . (d . (l + 1)) is set

gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() set

dom (q1 ^ <*gg*>) is Element of K19(NAT)

q1 . gg is set

l . gg is set

(q1 ^ <*gg*>) . gg is set

dom <*gg*> is non empty V12() V50(1) Element of K19(NAT)

(len q1) + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(q1 ^ <*gg*>) . ((len q1) + 1) is set

<*gg*> . 1 is set

{f} is non empty V12() V50(1) set

Seg (d1 + 1) is V43() V50(d1 + 1) Element of K19(NAT)

(Seg d1) \/ {f} is non empty set

gg is set

dom gg is set

gg . gg is set

i is set

gg . i is set

dom gg is Element of K19((dom (q1 ^ q2)))

K19((dom (q1 ^ q2))) is set

d . i is set

d . gg is set

j is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg . j is set

j1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg . j1 is set

a is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

j is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg . j is set

j1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg . j1 is set

b is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

b - 1 is ext-real V34() V42() set

(b - 1) + 1 is ext-real V34() V42() set

(Seg (d1 + 1)) \ (Seg d1) is Element of K19(NAT)

{(d1 + 1)} is non empty V12() V50(1) set

b is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

j is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg . j is set

a is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

a - 1 is ext-real V34() V42() set

j1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg . j1 is set

(a - 1) + 1 is ext-real V34() V42() set

(Seg (d1 + 1)) \ (Seg d1) is Element of K19(NAT)

{(d1 + 1)} is non empty V12() V50(1) set

j1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg . j1 is set

b is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

b - 1 is ext-real V34() V42() set

- 1 is ext-real non positive V34() V42() set

b + (- 1) is ext-real V34() V42() set

j is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg . j is set

a is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

a - 1 is ext-real V34() V42() set

a + (- 1) is ext-real V34() V42() set

(len (q1 ^ <*gg*>)) + (len q2) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(len q1) + (len <*gg*>) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

((len q1) + (len <*gg*>)) + d2 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

Seg ((len (q1 ^ <*gg*>)) + (len q2)) is V43() V50((len (q1 ^ <*gg*>)) + (len q2)) Element of K19(NAT)

(q1 ^ <*gg*>) ^ q2 is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

i is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

d . i is set

gg is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom (q1 ^ q2)),(dom (q1 ^ q2))))

gg . i is set

j is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l . j is set

q1 . j is set

g . i is set

k . i is set

l . (d . i) is set

(q1 ^ q2) . (gg . i) is set

j is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(d1 + 2) - 1 is ext-real V34() V42() set

j - 1 is ext-real V34() V42() set

j1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom (q1 ^ q2)),(dom (q1 ^ q2))))

gg . i is set

a is ext-real V34() V35() V36() V37() V41() V42() V43() V48() set

(len q1) + a is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g . i is set

k . i is set

l . (d . i) is set

<*gg*> ^ q2 is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

q1 ^ (<*gg*> ^ q2) is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

dom (<*gg*> ^ q2) is Element of K19(NAT)

b is ext-real V34() V35() V36() V37() V41() V42() V43() V48() set

(len q1) + b is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l . j is set

(<*gg*> ^ q2) . b is set

1 + a is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(q1 ^ q2) . (j - 1) is set

q2 . a is set

(q1 ^ q2) . (gg . i) is set

k . i is set

gg is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom (q1 ^ q2)),(dom (q1 ^ q2))))

gg . i is set

(q1 ^ q2) . (gg . i) is set

k . i is set

gg is Relation-like dom (q1 ^ q2) -defined dom (q1 ^ q2) -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom (q1 ^ q2)),(dom (q1 ^ q2))))

gg . i is set

(q1 ^ q2) . (gg . i) is set

k ^ <*gg*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

(D,k,k) is Element of D

(D,(q1 ^ q2),k) is Element of D

k . ((D,(q1 ^ q2),k),gg) is Element of D

<*gg*> ^ q2 is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

len (<*gg*> ^ q2) is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(len <*gg*>) + (len q2) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(D,q1,k) is Element of D

(D,q2,k) is Element of D

k . ((D,q1,k),(D,q2,k)) is Element of D

k . ((k . ((D,q1,k),(D,q2,k))),gg) is Element of D

k . ((D,q2,k),gg) is Element of D

k . ((D,q1,k),(k . ((D,q2,k),gg))) is Element of D

k . (gg,(D,q2,k)) is Element of D

k . ((D,q1,k),(k . (gg,(D,q2,k)))) is Element of D

(D,(<*gg*> ^ q2),k) is Element of D

k . ((D,q1,k),(D,(<*gg*> ^ q2),k)) is Element of D

q1 ^ (<*gg*> ^ q2) is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

(D,(q1 ^ (<*gg*> ^ q2)),k) is Element of D

<*gg*> ^ q2 is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

<*gg*> ^ (q1 ^ q2) is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

k . (gg,(D,(q1 ^ q2),k)) is Element of D

(D,(<*gg*> ^ (q1 ^ q2)),k) is Element of D

(q1 ^ q2) ^ <*gg*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

0 + 0 is Function-like functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-membered Element of NAT

d . 1 is set

l . 1 is set

g . 1 is set

l is Relation-like dom F -defined dom F -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom F),(dom F)))

l is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

dom l is Element of K19(NAT)

K20((dom l),(dom l)) is set

K19(K20((dom l),(dom l))) is set

len l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom g is Element of K19(NAT)

k is Relation-like dom l -defined dom l -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom l),(dom l)))

(D,l,k) is Element of D

(D,g,k) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

dom F is Element of K19(NAT)

K20((dom F),(dom F)) is set

K19(K20((dom F),(dom F))) is set

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,k) is Element of D

(D,g,k) is Element of D

l is Relation-like dom F -defined dom F -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom F),(dom F)))

l * F is Relation-like Function-like set

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

the_unity_wrt k is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

dom F is Element of K19(NAT)

K20((dom F),(dom F)) is set

K19(K20((dom F),(dom F))) is set

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,k) is Element of D

(D,g,k) is Element of D

l is Relation-like dom F -defined dom F -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom F),(dom F)))

l * F is Relation-like Function-like set

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom g is Element of K19(NAT)

l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g . l is set

l . l is set

F . (l . l) is set

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

rng F is set

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

rng g is set

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,k) is Element of D

(D,g,k) is Element of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

F " is Relation-like Function-like set

g * (F ") is Relation-like Function-like set

dom (F ") is set

dom (g * (F ")) is set

dom g is Element of K19(NAT)

Seg (len F) is V43() V50( len F) Element of K19(NAT)

dom F is Element of K19(NAT)

rng (F ") is set

rng (g * (F ")) is set

K20((dom F),(dom F)) is set

K19(K20((dom F),(dom F))) is set

l is Relation-like dom F -defined dom F -valued Function-like total quasi_total Element of K19(K20((dom F),(dom F)))

rng l is set

g is Relation-like dom F -defined dom F -valued Function-like one-to-one total quasi_total onto bijective Element of K19(K20((dom F),(dom F)))

g * F is Relation-like Function-like set

(F ") * F is Relation-like Function-like set

g * ((F ") * F) is Relation-like Function-like set

id (rng g) is Relation-like Function-like one-to-one set

g * (id (rng g)) is Relation-like Function-like set

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

rng F is set

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

rng g is set

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,k) is Element of D

(D,g,k) is Element of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

the_unity_wrt k is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

rng F is set

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

rng g is set

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,k) is Element of D

(D,g,k) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

F . 1 is set

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,g) is Element of D

<*(F . 1)*> is Relation-like NAT -defined Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like set

F /. 1 is Element of D

<*(F /. 1)*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom F is Element of K19(NAT)

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

k is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,k,l) is Element of D

(D,F,l) is Element of D

(D,g,l) is Element of D

l . ((D,F,l),(D,g,l)) is Element of D

l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l + 1 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom g is Element of K19(NAT)

(D,g,l) is Element of D

k is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(D,k,l) is Element of D

l . ((D,g,l),(D,k,l)) is Element of D

d is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len d is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(D,d,l) is Element of D

Seg l is V43() V50(l) Element of K19(NAT)

g | (Seg l) is Relation-like NAT -defined D -valued Function-like FinSubsequence-like Element of K19(K20(NAT,D))

K20(NAT,D) is V43() set

K19(K20(NAT,D)) is V43() set

k | (Seg l) is Relation-like NAT -defined D -valued Function-like FinSubsequence-like Element of K19(K20(NAT,D))

d | (Seg l) is Relation-like NAT -defined D -valued Function-like FinSubsequence-like Element of K19(K20(NAT,D))

h is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len h is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

f is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len f is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

gg is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len gg is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

Seg (len f) is V43() V50( len f) Element of K19(NAT)

Seg (len g) is V43() V50( len g) Element of K19(NAT)

dom f is Element of K19(NAT)

d is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

Seg (len gg) is V43() V50( len gg) Element of K19(NAT)

dom gg is Element of K19(NAT)

k . d is set

gg . d is set

Seg (len h) is V43() V50( len h) Element of K19(NAT)

dom h is Element of K19(NAT)

d . d is set

h . d is set

g . d is set

f . d is set

l . ((f . d),(gg . d)) is set

rng d is set

rng g is set

rng k is set

Seg (l + 1) is V43() V50(l + 1) Element of K19(NAT)

dom k is Element of K19(NAT)

k . (l + 1) is set

dom d is Element of K19(NAT)

d . (l + 1) is set

g . (l + 1) is set

d2 is Element of D

l . ((g . (l + 1)),(k . (l + 1))) is set

d is Element of D

<*d*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

f ^ <*d*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

(D,f,l) is Element of D

l . ((D,f,l),d) is Element of D

d1 is Element of D

<*d1*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

gg ^ <*d1*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

(D,gg,l) is Element of D

l . ((D,gg,l),d1) is Element of D

<*d2*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

h ^ <*d2*> is Relation-like NAT -defined D -valued Function-like non empty V43() FinSequence-like FinSubsequence-like FinSequence of D

(D,h,l) is Element of D

l . ((D,f,l),(D,gg,l)) is Element of D

l . (d,d1) is Element of D

l . ((l . ((D,f,l),(D,gg,l))),(l . (d,d1))) is Element of D

l . ((l . ((D,f,l),(D,gg,l))),d) is Element of D

l . ((l . ((l . ((D,f,l),(D,gg,l))),d)),d1) is Element of D

l . ((D,gg,l),d) is Element of D

l . ((D,f,l),(l . ((D,gg,l),d))) is Element of D

l . ((l . ((D,f,l),(l . ((D,gg,l),d)))),d1) is Element of D

l . (d,(D,gg,l)) is Element of D

l . ((D,f,l),(l . (d,(D,gg,l)))) is Element of D

l . ((l . ((D,f,l),(l . (d,(D,gg,l))))),d1) is Element of D

l . ((D,g,l),(D,gg,l)) is Element of D

l . ((l . ((D,g,l),(D,gg,l))),d1) is Element of D

k . 1 is set

d . 1 is set

g . 1 is set

l is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

k is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom l is Element of K19(NAT)

(D,k,l) is Element of D

(D,l,l) is Element of D

(D,g,l) is Element of D

l . ((D,l,l),(D,g,l)) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

k is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,l) is Element of D

(D,g,l) is Element of D

(D,k,l) is Element of D

l . ((D,g,l),(D,k,l)) is Element of D

the_unity_wrt l is Element of D

l . ((the_unity_wrt l),(the_unity_wrt l)) is Element of D

l . ((D,g,l),(the_unity_wrt l)) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len F is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

dom F is Element of K19(NAT)

g is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

k is Relation-like NAT -defined D -valued Function-like V43() FinSequence-like FinSubsequence-like FinSequence of D

len k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

l is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,F,l) is Element of D

(D,g,l) is Element of D

(D,k,l) is Element of D

l . ((D,g,l),(D,k,l)) is Element of D

Seg (len F) is V43() V50( len F) Element of K19(NAT)

dom g is Element of K19(NAT)

Seg (len g) is V43() V50( len g) Element of K19(NAT)

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

<*> D is Relation-like NAT -defined D -valued Function-like one-to-one constant functional empty ext-real non positive non negative V34() V35() V36() V37() V39() V40() V41() V42() V43() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of D

(D,(<*> D),F) is Element of D

the_unity_wrt F is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

<*F*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,<*F*>,g) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

g is Element of D

<*F,g*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(2) FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,<*F,g*>,k) is Element of D

k . (F,g) is Element of D

<*F*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

len <*F*> is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

<*g*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

<*F*> ^ <*g*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(1 + 1) FinSequence-like FinSubsequence-like FinSequence of D

1 + 1 is non empty ext-real positive non negative V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(D,(<*F*> ^ <*g*>),k) is Element of D

(D,<*F*>,k) is Element of D

k . ((D,<*F*>,k),g) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

g is Element of D

<*F,g*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(2) FinSequence-like FinSubsequence-like FinSequence of D

<*g,F*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(2) FinSequence-like FinSubsequence-like FinSequence of D

k is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,<*F,g*>,k) is Element of D

(D,<*g,F*>,k) is Element of D

k . (F,g) is Element of D

k . (g,F) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

g is Element of D

k is Element of D

<*F,g,k*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(3) FinSequence-like FinSubsequence-like FinSequence of D

l is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,<*F,g,k*>,l) is Element of D

l . (F,g) is Element of D

l . ((l . (F,g)),k) is Element of D

<*F,g*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(2) FinSequence-like FinSubsequence-like FinSequence of D

len <*F,g*> is non empty ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

<*k*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

<*F,g*> ^ <*k*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(2 + 1) FinSequence-like FinSubsequence-like FinSequence of D

2 + 1 is non empty ext-real positive non negative V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

(D,(<*F,g*> ^ <*k*>),l) is Element of D

(D,<*F,g*>,l) is Element of D

l . ((D,<*F,g*>,l),k) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

g is Element of D

k is Element of D

<*F,g,k*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(3) FinSequence-like FinSubsequence-like FinSequence of D

<*g,F,k*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(3) FinSequence-like FinSubsequence-like FinSequence of D

l is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,<*F,g,k*>,l) is Element of D

(D,<*g,F,k*>,l) is Element of D

l . (F,g) is Element of D

l . ((l . (F,g)),k) is Element of D

l . (g,F) is Element of D

l . ((l . (g,F)),k) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

1 |-> F is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on D

1 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(1 |-> F),g) is Element of D

<*F*> is Relation-like NAT -defined D -valued Function-like constant non empty V12() V43() V50(1) FinSequence-like FinSubsequence-like FinSequence of D

(D,<*F*>,g) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

2 |-> F is Relation-like NAT -defined D -valued Function-like V43() V50(2) FinSequence-like FinSubsequence-like Element of 2 -tuples_on D

2 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

(D,(2 |-> F),g) is Element of D

g . (F,F) is Element of D

<*F,F*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(2) FinSequence-like FinSubsequence-like FinSequence of D

(D,<*F,F*>,g) is Element of D

D is non empty set

K20(D,D) is set

K20(K20(D,D),D) is set

K19(K20(K20(D,D),D)) is set

F is Element of D

g is Relation-like K20(D,D) -defined D -valued Function-like total quasi_total Element of K19(K20(K20(D,D),D))

k is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

k |-> F is Relation-like NAT -defined D -valued Function-like V43() V50(k) FinSequence-like FinSubsequence-like Element of k -tuples_on D

k -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D

(D,(k |-> F),g) is Element of D

l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT

k + l is ext-real