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 V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT
(k + l) |-> F is Relation-like NAT -defined D -valued Function-like V43() V50(k + l) FinSequence-like FinSubsequence-like Element of (k + l) -tuples_on D
(k + l) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,((k + l) |-> F),g) is Element of D
l |-> F is Relation-like NAT -defined D -valued Function-like V43() V50(l) FinSequence-like FinSubsequence-like Element of l -tuples_on D
l -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,(l |-> F),g) is Element of D
g . ((D,(k |-> F),g),(D,(l |-> F),g)) is Element of D
len (k |-> F) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT
len (l |-> F) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT
(k |-> F) ^ (l |-> F) is Relation-like NAT -defined D -valued Function-like V43() V50(k + l) FinSequence-like FinSubsequence-like FinSequence of D
k + l is ext-real V34() V35() V36() V37() V41() V42() V43() V48() 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
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 V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT
(k * l) |-> F is Relation-like NAT -defined D -valued Function-like V43() V50(k * l) FinSequence-like FinSubsequence-like Element of (k * l) -tuples_on D
(k * l) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,((k * l) |-> F),g) is Element of D
l |-> (D,(k |-> F),g) is Relation-like NAT -defined D -valued Function-like V43() V50(l) FinSequence-like FinSubsequence-like Element of l -tuples_on D
l -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,(l |-> (D,(k |-> F),g)),g) 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 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 * (l + 1) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT
d is Element of D
(k * (l + 1)) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(k * (l + 1)) FinSequence-like FinSubsequence-like Element of (k * (l + 1)) -tuples_on D
(k * (l + 1)) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,((k * (l + 1)) |-> d),g) is Element of D
k |-> d 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 |-> d),g) is Element of D
(l + 1) |-> (D,(k |-> d),g) is Relation-like NAT -defined D -valued Function-like V43() V50(l + 1) FinSequence-like FinSubsequence-like Element of (l + 1) -tuples_on D
(l + 1) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,((l + 1) |-> (D,(k |-> d),g)),g) is Element of D
k * l 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
(k * l) + (k * 1) is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT
((k * l) + (k * 1)) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50((k * l) + (k * 1)) FinSequence-like FinSubsequence-like Element of ((k * l) + (k * 1)) -tuples_on D
((k * l) + (k * 1)) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,(((k * l) + (k * 1)) |-> d),g) is Element of D
(k * l) |-> d is Relation-like NAT -defined D -valued Function-like V43() V50(k * l) FinSequence-like FinSubsequence-like Element of (k * l) -tuples_on D
(k * l) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,((k * l) |-> d),g) is Element of D
g . ((D,((k * l) |-> d),g),(D,(k |-> d),g)) is Element of D
l |-> (D,(k |-> d),g) is Relation-like NAT -defined D -valued Function-like V43() V50(l) FinSequence-like FinSubsequence-like Element of l -tuples_on D
l -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,(l |-> (D,(k |-> d),g)),g) is Element of D
g . ((D,(l |-> (D,(k |-> d),g)),g),(D,(k |-> d),g)) is Element of D
1 |-> (D,(k |-> d),g) 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
(D,(1 |-> (D,(k |-> d),g)),g) is Element of D
g . ((D,(l |-> (D,(k |-> d),g)),g),(D,(1 |-> (D,(k |-> d),g)),g)) is Element 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))
g is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT
g * 0 is ext-real V34() V35() V36() V37() V41() V42() V43() V48() Element of NAT
k is Element of D
(g * 0) |-> k is Relation-like NAT -defined D -valued Function-like V43() V50(g * 0) FinSequence-like FinSubsequence-like Element of (g * 0) -tuples_on D
(g * 0) -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,((g * 0) |-> k),l) is Element of D
g |-> k is Relation-like NAT -defined D -valued Function-like V43() V50(g) FinSequence-like FinSubsequence-like Element of g -tuples_on D
g -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,(g |-> k),l) is Element of D
0 |-> (D,(g |-> k),l) 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( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered Element of 0 -tuples_on D
0 -tuples_on D is functional non empty FinSequence-membered FinSequenceSet of D
(D,(0 |-> (D,(g |-> k),l)),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 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 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 . 1 is set
F . 2 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
g . ((F . 1),(F . 2)) is set
<*(F . 1),(F . 2)*> is Relation-like NAT -defined Function-like non empty V43() V50(2) FinSequence-like FinSubsequence-like set
F /. 1 is Element of D
<*(F /. 1),(F . 2)*> is Relation-like NAT -defined Function-like non empty V43() V50(2) FinSequence-like FinSubsequence-like set
F /. 2 is Element of D
<*(F /. 1),(F /. 2)*> is Relation-like NAT -defined D -valued Function-like non empty V43() V50(2) FinSequence-like FinSubsequence-like FinSequence of D
g . ((F /. 1),(F /. 2)) is Element of D
g . ((F . 1),(F /. 2)) is set