:: BHSP_5 semantic presentation

REAL is non empty V12() V43() V44() V45() V49() non finite set
NAT is non empty V12() V29() V30() V31() V43() V44() V45() V46() V47() V48() V49() non finite cardinal limit_cardinal Element of K19(REAL)
K19(REAL) is V12() non finite set
{} is Function-like functional empty V29() V30() V31() V33() V34() V35() V43() V44() V45() V46() V47() V48() V49() finite V54() cardinal {} -element set
COMPLEX is non empty V12() V43() V49() non finite set
RAT is non empty V12() V43() V44() V45() V46() V49() non finite set
INT is non empty V12() V43() V44() V45() V46() V47() V49() non finite set
K20(COMPLEX,COMPLEX) is V12() non finite set
K19(K20(COMPLEX,COMPLEX)) is V12() non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V12() non finite set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() non finite set
K20(REAL,REAL) is V12() non finite set
K19(K20(REAL,REAL)) is V12() non finite set
K20(K20(REAL,REAL),REAL) is V12() non finite set
K19(K20(K20(REAL,REAL),REAL)) is V12() non finite set
K20(RAT,RAT) is V12() non finite set
K19(K20(RAT,RAT)) is V12() non finite set
K20(K20(RAT,RAT),RAT) is V12() non finite set
K19(K20(K20(RAT,RAT),RAT)) is V12() non finite set
K20(INT,INT) is V12() non finite set
K19(K20(INT,INT)) is V12() non finite set
K20(K20(INT,INT),INT) is V12() non finite set
K19(K20(K20(INT,INT),INT)) is V12() non finite set
K20(NAT,NAT) is V12() non finite set
K20(K20(NAT,NAT),NAT) is V12() non finite set
K19(K20(K20(NAT,NAT),NAT)) is V12() non finite set
NAT is non empty V12() V29() V30() V31() V43() V44() V45() V46() V47() V48() V49() non finite cardinal limit_cardinal set
K19(NAT) is V12() non finite set
K19(NAT) is V12() non finite set
K118(NAT) is V27() set
K20(NAT,REAL) is V12() non finite set
K19(K20(NAT,REAL)) is V12() non finite set
1 is non empty V29() V30() V31() V35() V36() V37() ext-real positive V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
0 is Function-like functional empty V29() V30() V31() V33() V34() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() V49() finite V54() cardinal {} -element Element of NAT
2 is non empty V29() V30() V31() V35() V36() V37() ext-real positive V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT

DK is set

rng DX is set
rng f is set
dom DX is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
dom f is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
K20((dom DX),(dom DX)) is set
K19(K20((dom DX),(dom DX))) is set

f * (DX ") is Relation-like Function-like set
len DX is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
card (rng f) is V29() V30() V31() cardinal set
len f is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Seg (len f) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
dom (DX ") is set
Y2 is set
f . Y2 is set
dom (f * (DX ")) is set
rng (DX ") is set
rng (f * (DX ")) is set
Y2 is set
Y2 is set
F is set
(DX ") . F is set
Z is set
f . Z is set
(f * (DX ")) . Z is set
Y2 is set
(f * (DX ")) . Y2 is set
(f * (DX ")) * DX is Relation-like Function-like set
dom ((f * (DX ")) * DX) is set
Y2 is set
f . Y2 is set
((f * (DX ")) * DX) . Y2 is set
(f * (DX ")) . Y2 is set
DX . ((f * (DX ")) . Y2) is set
(DX ") . (f . Y2) is set
DX . ((DX ") . (f . Y2)) is set
DK is non empty set
K20(DK,DK) is set
K20(K20(DK,DK),DK) is set
K19(K20(K20(DK,DK),DK)) is set
DX is Relation-like K20(DK,DK) -defined DK -valued Function-like V14(K20(DK,DK)) quasi_total Element of K19(K20(K20(DK,DK),DK))
K19(DK) is set
f is finite Element of K19(DK)

rng Y1 is set

DX "**" Y2 is Element of DK

rng F is set
DX "**" F is Element of DK
Y1 is Element of DK
Y2 is Element of DK

rng F is set
DX "**" F is Element of DK

rng F is set
DX "**" F is Element of DK

rng Z is set
DX "**" Z is Element of DK

rng Z is set
DX "**" Z is Element of DK
dom F is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
K20((dom F),(dom F)) is set
K19(K20((dom F),(dom F))) is set

dom p1 is set
rng p1 is set

the carrier of DK is non empty set
K19( the carrier of DK) is set
DX is finite Element of K19( the carrier of DK)
the addF of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK))
K20( the carrier of DK, the carrier of DK) is set
K20(K20( the carrier of DK, the carrier of DK), the carrier of DK) is set
K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK)) is set
( the carrier of DK, the addF of DK,DX) is Element of the carrier of DK
0. DK is V69(DK) Element of the carrier of DK

the carrier of DK is non empty set
the scalar of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined REAL -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK),REAL))
K20( the carrier of DK, the carrier of DK) is set
K20(K20( the carrier of DK, the carrier of DK),REAL) is set
K19(K20(K20( the carrier of DK, the carrier of DK),REAL)) is set
DX is Element of the carrier of DK

Y1 is V29() V30() V31() V35() finite cardinal set
f . Y1 is set
[DX,(f . Y1)] is set
{DX,(f . Y1)} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,(f . Y1)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(f . Y1)] is set
DX is non empty set
DK is non empty set
K20(DX,DK) is set
K19(K20(DX,DK)) is set

f is Relation-like DX -defined DK -valued Function-like non empty V14(DX) quasi_total Element of K19(K20(DX,DK))

DK is non empty set
K20(DK,DK) is set
K20(K20(DK,DK),DK) is set
K19(K20(K20(DK,DK),DK)) is set
f is Relation-like K20(DK,DK) -defined DK -valued Function-like V14(K20(DK,DK)) quasi_total Element of K19(K20(K20(DK,DK),DK))
DX is non empty set
K19(DX) is set
K20(DX,DK) is set
K19(K20(DX,DK)) is set
Y1 is finite Element of K19(DX)
Y2 is Relation-like DX -defined DK -valued Function-like non empty V14(DX) quasi_total Element of K19(K20(DX,DK))
dom Y2 is set

rng F is set

(DK,DX,Y2,Z) is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

f "**" (DK,DX,Y2,Z) is Element of DK

rng p1 is set
(DK,DX,Y2,p1) is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

f "**" (DK,DX,Y2,p1) is Element of DK
F is Element of DK
Z is Element of DK

rng p1 is set
(DK,DX,Y2,p1) is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

f "**" (DK,DX,Y2,p1) is Element of DK

rng p1 is set
(DK,DX,Y2,p1) is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

f "**" (DK,DX,Y2,p1) is Element of DK

rng p2 is set
(DK,DX,Y2,p2) is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

f "**" (DK,DX,Y2,p2) is Element of DK

rng p2 is set
(DK,DX,Y2,p2) is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

f "**" (DK,DX,Y2,p2) is Element of DK
dom p1 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
dom p2 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
K20((dom p1),(dom p1)) is set
K19(K20((dom p1),(dom p1))) is set
q is Relation-like dom p1 -defined dom p1 -valued Function-like one-to-one V14( dom p1) quasi_total onto bijective Element of K19(K20((dom p1),(dom p1)))

dom q is set
rng q is set
s is set
p1 . s is set
dom (DK,DX,Y2,p1) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
s is set
p2 . s is set
dom (DK,DX,Y2,p2) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
s is set
q . s is set
q * (DK,DX,Y2,p1) is Relation-like Function-like set
dom (q * (DK,DX,Y2,p1)) is set
s is set
t is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
q . t is set
j is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
(DK,DX,Y2,p2) . s is set
p2 . t is set
Y2 . (p2 . t) is set
p1 . (q . t) is set
Y2 . (p1 . (q . t)) is set
(DK,DX,Y2,p1) . j is set
(q * (DK,DX,Y2,p1)) . s is set

the carrier of DK is non empty set
K19( the carrier of DK) is set
f is finite Element of K19( the carrier of DK)
DX is Element of the carrier of DK

rng Y1 is set
Y2 is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK
len Y2 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT

len Z is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
dom Z is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
Seg (len Y2) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
dom Y2 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
p1 is V29() V30() V31() V35() finite cardinal set
Z . p1 is set
(DK,DX,Y2,p1) is set
the scalar of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined REAL -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK),REAL))
K20( the carrier of DK, the carrier of DK) is set
K20(K20( the carrier of DK, the carrier of DK),REAL) is set
K19(K20(K20( the carrier of DK, the carrier of DK),REAL)) is set
Y2 . p1 is set
[DX,(Y2 . p1)] is set
{DX,(Y2 . p1)} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,(Y2 . p1)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . p1)] is set
p2 is Element of the carrier of DK
DX .|. p2 is V36() V37() ext-real Element of REAL

addreal "**" p1 is V36() V37() ext-real Element of REAL
rng Y2 is set
dom p1 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
p2 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
p1 . p2 is set
(DK,DX,Y2,p2) is set
Y2 . p2 is set
[DX,(Y2 . p2)] is set
{DX,(Y2 . p2)} is non empty finite set
{{DX,(Y2 . p2)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . p2)] is set
Y1 is V36() V37() ext-real Element of REAL
Y2 is V36() V37() ext-real Element of REAL

rng F is set

dom Z is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
dom F is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
addreal "**" Z is V36() V37() ext-real Element of REAL

rng F is set
dom F is V43() V44() V45() V46() V47() V48() Element of K19(NAT)

rng Z is set

dom p1 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
dom Z is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
addreal "**" p1 is V36() V37() ext-real Element of REAL

rng Z is set
dom Z is V43() V44() V45() V46() V47() V48() Element of K19(NAT)

dom p1 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
addreal "**" p1 is V36() V37() ext-real Element of REAL

dom p1 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
addreal "**" p1 is V36() V37() ext-real Element of REAL

dom p2 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
addreal "**" p2 is V36() V37() ext-real Element of REAL

dom p2 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
addreal "**" p2 is V36() V37() ext-real Element of REAL
K20((dom F),(dom F)) is set
K19(K20((dom F),(dom F))) is set

dom q is set
rng q is set
s is set
q . s is set

dom (q * p1) is set
s is set
t is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
q . t is set
p2 . s is set
(DK,DX,Z,t) is set
the scalar of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined REAL -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK),REAL))
K20( the carrier of DK, the carrier of DK) is set
K20(K20( the carrier of DK, the carrier of DK),REAL) is set
K19(K20(K20( the carrier of DK, the carrier of DK),REAL)) is set
Z . t is set
[DX,(Z . t)] is set
{DX,(Z . t)} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,(Z . t)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Z . t)] is set
j is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
(DK,DX,F,j) is set
F . j is set
[DX,(F . j)] is set
{DX,(F . j)} is non empty finite set
{{DX,(F . j)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(F . j)] is set
p1 . (q . t) is set
(q * p1) . s is set

the carrier of DK is non empty set
K19( the carrier of DK) is set
f is finite Element of K19( the carrier of DK)
DX is Element of the carrier of DK
(DK,DX,f) is V36() V37() ext-real Element of REAL

the carrier of DK is non empty set
K19( the carrier of DK) is set
DX is Element of the carrier of DK
f is Element of the carrier of DK
DX .|. f is V36() V37() ext-real Element of REAL

the carrier of DK is non empty set
K19( the carrier of DK) is set
DX is Element of the carrier of DK
f is Element of the carrier of DK
DX .|. f is V36() V37() ext-real Element of REAL

the carrier of DK is non empty set
K19( the carrier of DK) is set

the carrier of DK is non empty set
K19( the carrier of DK) is set
DX is Element of the carrier of DK
DX .|. DX is V36() V37() ext-real Element of REAL

the carrier of DK is non empty set
DX is Element of the carrier of DK
DX .|. DX is V36() V37() ext-real Element of REAL

the carrier of DK is non empty set
K19( the carrier of DK) is set

the carrier of DK is non empty set
0. DK is V69(DK) Element of the carrier of DK
DX is Element of the carrier of DK
DX .|. DX is V36() V37() ext-real Element of REAL
f is Element of the carrier of DK
DX .|. f is V36() V37() ext-real Element of REAL
Y1 is Element of the carrier of DK
DX .|. Y1 is V36() V37() ext-real Element of REAL

the carrier of DK is non empty set
DX is Element of the carrier of DK
||.DX.|| is V36() V37() ext-real Element of REAL
||.DX.|| ^2 is V36() V37() ext-real Element of REAL
K143(||.DX.||,||.DX.||) is set
2 * (||.DX.|| ^2) is V36() V37() ext-real Element of REAL
f is Element of the carrier of DK
DX + f is Element of the carrier of DK
the addF of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK))
K20( the carrier of DK, the carrier of DK) is set
K20(K20( the carrier of DK, the carrier of DK), the carrier of DK) is set
K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK)) is set
the addF of DK . (DX,f) is Element of the carrier of DK
[DX,f] is set
{DX,f} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,f},{DX}} is non empty finite V54() set
the addF of DK . [DX,f] is set
||.(DX + f).|| is V36() V37() ext-real Element of REAL
||.(DX + f).|| ^2 is V36() V37() ext-real Element of REAL
K143(||.(DX + f).||,||.(DX + f).||) is set
DX - f is Element of the carrier of DK
- f is Element of the carrier of DK
DX + (- f) is Element of the carrier of DK
the addF of DK . (DX,(- f)) is Element of the carrier of DK
[DX,(- f)] is set
{DX,(- f)} is non empty finite set
{{DX,(- f)},{DX}} is non empty finite V54() set
the addF of DK . [DX,(- f)] is set
||.(DX - f).|| is V36() V37() ext-real Element of REAL
||.(DX - f).|| ^2 is V36() V37() ext-real Element of REAL
K143(||.(DX - f).||,||.(DX - f).||) is set
(||.(DX + f).|| ^2) + (||.(DX - f).|| ^2) is V36() V37() ext-real Element of REAL
is V36() V37() ext-real Element of REAL
^2 is V36() V37() ext-real Element of REAL
K143(,) is set
2 * () is V36() V37() ext-real Element of REAL
(2 * (||.DX.|| ^2)) + (2 * ()) is V36() V37() ext-real Element of REAL
(DX + f) .|. (DX + f) is V36() V37() ext-real Element of REAL
(DX - f) .|. (DX - f) is V36() V37() ext-real Element of REAL
DX .|. DX is V36() V37() ext-real Element of REAL
f .|. f is V36() V37() ext-real Element of REAL
sqrt ((DX + f) .|. (DX + f)) is V36() V37() ext-real Element of REAL
(sqrt ((DX + f) .|. (DX + f))) ^2 is V36() V37() ext-real Element of REAL
K143((sqrt ((DX + f) .|. (DX + f))),(sqrt ((DX + f) .|. (DX + f)))) is set
((sqrt ((DX + f) .|. (DX + f))) ^2) + (||.(DX - f).|| ^2) is V36() V37() ext-real Element of REAL
((DX + f) .|. (DX + f)) + (||.(DX - f).|| ^2) is V36() V37() ext-real Element of REAL
sqrt ((DX - f) .|. (DX - f)) is V36() V37() ext-real Element of REAL
(sqrt ((DX - f) .|. (DX - f))) ^2 is V36() V37() ext-real Element of REAL
K143((sqrt ((DX - f) .|. (DX - f))),(sqrt ((DX - f) .|. (DX - f)))) is set
((DX + f) .|. (DX + f)) + ((sqrt ((DX - f) .|. (DX - f))) ^2) is V36() V37() ext-real Element of REAL
((DX + f) .|. (DX + f)) + ((DX - f) .|. (DX - f)) is V36() V37() ext-real Element of REAL
DX .|. f is V36() V37() ext-real Element of REAL
2 * (DX .|. f) is V36() V37() ext-real Element of REAL
(DX .|. DX) + (2 * (DX .|. f)) is V36() V37() ext-real Element of REAL
((DX .|. DX) + (2 * (DX .|. f))) + (f .|. f) is V36() V37() ext-real Element of REAL
(((DX .|. DX) + (2 * (DX .|. f))) + (f .|. f)) + ((DX - f) .|. (DX - f)) is V36() V37() ext-real Element of REAL
(DX .|. DX) - (2 * (DX .|. f)) is V36() V37() ext-real Element of REAL
((DX .|. DX) - (2 * (DX .|. f))) + (f .|. f) is V36() V37() ext-real Element of REAL
(((DX .|. DX) + (2 * (DX .|. f))) + (f .|. f)) + (((DX .|. DX) - (2 * (DX .|. f))) + (f .|. f)) is V36() V37() ext-real Element of REAL
2 * (DX .|. DX) is V36() V37() ext-real Element of REAL
2 * (f .|. f) is V36() V37() ext-real Element of REAL
(2 * (DX .|. DX)) + (2 * (f .|. f)) is V36() V37() ext-real Element of REAL
sqrt (DX .|. DX) is V36() V37() ext-real Element of REAL
(sqrt (DX .|. DX)) ^2 is V36() V37() ext-real Element of REAL
K143((sqrt (DX .|. DX)),(sqrt (DX .|. DX))) is set
2 * ((sqrt (DX .|. DX)) ^2) is V36() V37() ext-real Element of REAL
(2 * ((sqrt (DX .|. DX)) ^2)) + (2 * (f .|. f)) is V36() V37() ext-real Element of REAL
sqrt (f .|. f) is V36() V37() ext-real Element of REAL
(sqrt (f .|. f)) ^2 is V36() V37() ext-real Element of REAL
K143((sqrt (f .|. f)),(sqrt (f .|. f))) is set
2 * ((sqrt (f .|. f)) ^2) is V36() V37() ext-real Element of REAL
(2 * ((sqrt (DX .|. DX)) ^2)) + (2 * ((sqrt (f .|. f)) ^2)) is V36() V37() ext-real Element of REAL
(2 * (||.DX.|| ^2)) + (2 * ((sqrt (f .|. f)) ^2)) is V36() V37() ext-real Element of REAL

the carrier of DK is non empty set
DX is Element of the carrier of DK
||.DX.|| is V36() V37() ext-real Element of REAL
||.DX.|| ^2 is V36() V37() ext-real Element of REAL
K143(||.DX.||,||.DX.||) is set
f is Element of the carrier of DK
DX + f is Element of the carrier of DK
the addF of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK))
K20( the carrier of DK, the carrier of DK) is set
K20(K20( the carrier of DK, the carrier of DK), the carrier of DK) is set
K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK)) is set
the addF of DK . (DX,f) is Element of the carrier of DK
[DX,f] is set
{DX,f} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,f},{DX}} is non empty finite V54() set
the addF of DK . [DX,f] is set
||.(DX + f).|| is V36() V37() ext-real Element of REAL
||.(DX + f).|| ^2 is V36() V37() ext-real Element of REAL
K143(||.(DX + f).||,||.(DX + f).||) is set
is V36() V37() ext-real Element of REAL
^2 is V36() V37() ext-real Element of REAL
K143(,) is set
(||.DX.|| ^2) + () is V36() V37() ext-real Element of REAL
DX .|. f is V36() V37() ext-real Element of REAL
(DX + f) .|. (DX + f) is V36() V37() ext-real Element of REAL
DX .|. DX is V36() V37() ext-real Element of REAL
f .|. f is V36() V37() ext-real Element of REAL
sqrt ((DX + f) .|. (DX + f)) is V36() V37() ext-real Element of REAL
(sqrt ((DX + f) .|. (DX + f))) ^2 is V36() V37() ext-real Element of REAL
K143((sqrt ((DX + f) .|. (DX + f))),(sqrt ((DX + f) .|. (DX + f)))) is set
2 * (DX .|. f) is V36() V37() ext-real Element of REAL
(DX .|. DX) + (2 * (DX .|. f)) is V36() V37() ext-real Element of REAL
((DX .|. DX) + (2 * (DX .|. f))) + (f .|. f) is V36() V37() ext-real Element of REAL
sqrt (DX .|. DX) is V36() V37() ext-real Element of REAL
(sqrt (DX .|. DX)) ^2 is V36() V37() ext-real Element of REAL
K143((sqrt (DX .|. DX)),(sqrt (DX .|. DX))) is set
((sqrt (DX .|. DX)) ^2) + (f .|. f) is V36() V37() ext-real Element of REAL
sqrt (f .|. f) is V36() V37() ext-real Element of REAL
(sqrt (f .|. f)) ^2 is V36() V37() ext-real Element of REAL
K143((sqrt (f .|. f)),(sqrt (f .|. f))) is set
((sqrt (DX .|. DX)) ^2) + ((sqrt (f .|. f)) ^2) is V36() V37() ext-real Element of REAL
(||.DX.|| ^2) + ((sqrt (f .|. f)) ^2) is V36() V37() ext-real Element of REAL

the carrier of DK is non empty set
the scalar of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined REAL -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK),REAL))
K20( the carrier of DK, the carrier of DK) is set
K20(K20( the carrier of DK, the carrier of DK),REAL) is set
K19(K20(K20( the carrier of DK, the carrier of DK),REAL)) is set
the addF of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK))
K20(K20( the carrier of DK, the carrier of DK), the carrier of DK) is set
K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK)) is set
DX is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK
len DX is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
dom DX is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
the addF of DK "**" DX is Element of the carrier of DK
( the addF of DK "**" DX) .|. ( the addF of DK "**" DX) is V36() V37() ext-real Element of REAL

dom f is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
addreal "**" f is V36() V37() ext-real Element of REAL
K20(NAT, the carrier of DK) is V12() non finite set
K19(K20(NAT, the carrier of DK)) is V12() non finite set
DX . 1 is set
Y1 is Relation-like NAT -defined the carrier of DK -valued Function-like non empty V14( NAT ) quasi_total Element of K19(K20(NAT, the carrier of DK))
Y1 . 1 is set
Y1 . (len DX) is set
[(Y1 . (len DX)),(Y1 . (len DX))] is set
{(Y1 . (len DX)),(Y1 . (len DX))} is non empty finite set
{(Y1 . (len DX))} is non empty V12() finite 1 -element set
{{(Y1 . (len DX)),(Y1 . (len DX))},{(Y1 . (len DX))}} is non empty finite V54() set
the scalar of DK . [(Y1 . (len DX)),(Y1 . (len DX))] is set
len f is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Seg (len f) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
Seg (len DX) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
f . 1 is set

Y2 . 1 is set
Y2 . (len f) is set
Y2 . 0 is set
Y1 . 0 is set
[(Y1 . 0),(Y1 . 0)] is set
{(Y1 . 0),(Y1 . 0)} is non empty finite set
{(Y1 . 0)} is non empty V12() finite 1 -element set
{{(Y1 . 0),(Y1 . 0)},{(Y1 . 0)}} is non empty finite V54() set
the scalar of DK . [(Y1 . 0),(Y1 . 0)] is set
F is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Y2 . F is set
Y1 . F is set
[(Y1 . F),(Y1 . F)] is set
{(Y1 . F),(Y1 . F)} is non empty finite set
{(Y1 . F)} is non empty V12() finite 1 -element set
{{(Y1 . F),(Y1 . F)},{(Y1 . F)}} is non empty finite V54() set
the scalar of DK . [(Y1 . F),(Y1 . F)] is set
F + 1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Y2 . (F + 1) is set
Y1 . (F + 1) is set
[(Y1 . (F + 1)),(Y1 . (F + 1))] is set
{(Y1 . (F + 1)),(Y1 . (F + 1))} is non empty finite set
{(Y1 . (F + 1))} is non empty V12() finite 1 -element set
{{(Y1 . (F + 1)),(Y1 . (F + 1))},{(Y1 . (F + 1))}} is non empty finite V54() set
the scalar of DK . [(Y1 . (F + 1)),(Y1 . (F + 1))] is set
0 + 1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
(len f) - 0 is V36() V37() ext-real V41() V42() Element of INT
(F + 1) - 1 is V36() V37() ext-real V41() V42() Element of INT
dom Y1 is set
rng Y1 is set
DX . (F + 1) is set
rng DX is set
p1 is Element of the carrier of DK
p2 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Y1 . p2 is set
[(Y1 . p2),p1] is set
{(Y1 . p2),p1} is non empty finite set
{(Y1 . p2)} is non empty V12() finite 1 -element set
{{(Y1 . p2),p1},{(Y1 . p2)}} is non empty finite V54() set
the scalar of DK . [(Y1 . p2),p1] is set
[(Y1 . 0),p1] is set
{(Y1 . 0),p1} is non empty finite set
{{(Y1 . 0),p1},{(Y1 . 0)}} is non empty finite V54() set
the scalar of DK . [(Y1 . 0),p1] is set
q is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Y1 . q is set
[(Y1 . q),p1] is set
{(Y1 . q),p1} is non empty finite set
{(Y1 . q)} is non empty V12() finite 1 -element set
{{(Y1 . q),p1},{(Y1 . q)}} is non empty finite V54() set
the scalar of DK . [(Y1 . q),p1] is set
q + 1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Y1 . (q + 1) is set
[(Y1 . (q + 1)),p1] is set
{(Y1 . (q + 1)),p1} is non empty finite set
{(Y1 . (q + 1))} is non empty V12() finite 1 -element set
{{(Y1 . (q + 1)),p1},{(Y1 . (q + 1))}} is non empty finite V54() set
the scalar of DK . [(Y1 . (q + 1)),p1] is set
DX . (q + 1) is set
(len DX) - 0 is V36() V37() ext-real V41() V42() Element of INT
(q + 1) - 1 is V36() V37() ext-real V41() V42() Element of INT
s is Element of the carrier of DK
s .|. p1 is V36() V37() ext-real Element of REAL
(q + 1) + 0 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
t is Element of the carrier of DK
s + t is Element of the carrier of DK
the addF of DK . (s,t) is Element of the carrier of DK
[s,t] is set
{s,t} is non empty finite set
{s} is non empty V12() finite 1 -element set
{{s,t},{s}} is non empty finite V54() set
the addF of DK . [s,t] is set
[(s + t),p1] is set
{(s + t),p1} is non empty finite set
{(s + t)} is non empty V12() finite 1 -element set
{{(s + t),p1},{(s + t)}} is non empty finite V54() set
the scalar of DK . [(s + t),p1] is set
(s + t) .|. p1 is V36() V37() ext-real Element of REAL
t .|. p1 is V36() V37() ext-real Element of REAL
0 + (t .|. p1) is V36() V37() ext-real Element of REAL
[t,p1] is set
{t,p1} is non empty finite set
{t} is non empty V12() finite 1 -element set
{{t,p1},{t}} is non empty finite V54() set
the scalar of DK . [t,p1] is set
Z is Element of the carrier of DK
[Z,p1] is set
{Z,p1} is non empty finite set
{Z} is non empty V12() finite 1 -element set
{{Z,p1},{Z}} is non empty finite V54() set
the scalar of DK . [Z,p1] is set
Z .|. p1 is V36() V37() ext-real Element of REAL
Y2 . (F + 1) is set
f . (F + 1) is set
addreal . (( the scalar of DK . [(Y1 . F),(Y1 . F)]),(f . (F + 1))) is set
[( the scalar of DK . [(Y1 . F),(Y1 . F)]),(f . (F + 1))] is set
{( the scalar of DK . [(Y1 . F),(Y1 . F)]),(f . (F + 1))} is non empty finite set
{( the scalar of DK . [(Y1 . F),(Y1 . F)])} is non empty V12() finite 1 -element set
{{( the scalar of DK . [(Y1 . F),(Y1 . F)]),(f . (F + 1))},{( the scalar of DK . [(Y1 . F),(Y1 . F)])}} is non empty finite V54() set
addreal . [( the scalar of DK . [(Y1 . F),(Y1 . F)]),(f . (F + 1))] is set
[(DX . (F + 1)),(DX . (F + 1))] is set
{(DX . (F + 1)),(DX . (F + 1))} is non empty finite set
{(DX . (F + 1))} is non empty V12() finite 1 -element set
{{(DX . (F + 1)),(DX . (F + 1))},{(DX . (F + 1))}} is non empty finite V54() set
the scalar of DK . [(DX . (F + 1)),(DX . (F + 1))] is set
addreal . (( the scalar of DK . [(Y1 . F),(Y1 . F)]),( the scalar of DK . [(DX . (F + 1)),(DX . (F + 1))])) is set
[( the scalar of DK . [(Y1 . F),(Y1 . F)]),( the scalar of DK . [(DX . (F + 1)),(DX . (F + 1))])] is set
{( the scalar of DK . [(Y1 . F),(Y1 . F)]),( the scalar of DK . [(DX . (F + 1)),(DX . (F + 1))])} is non empty finite set
{{( the scalar of DK . [(Y1 . F),(Y1 . F)]),( the scalar of DK . [(DX . (F + 1)),(DX . (F + 1))])},{( the scalar of DK . [(Y1 . F),(Y1 . F)])}} is non empty finite V54() set
addreal . [( the scalar of DK . [(Y1 . F),(Y1 . F)]),( the scalar of DK . [(DX . (F + 1)),(DX . (F + 1))])] is set
p1 .|. p1 is V36() V37() ext-real Element of REAL
addreal . (( the scalar of DK . [(Y1 . F),(Y1 . F)]),(p1 .|. p1)) is set
[( the scalar of DK . [(Y1 . F),(Y1 . F)]),(p1 .|. p1)] is set
{( the scalar of DK . [(Y1 . F),(Y1 . F)]),(p1 .|. p1)} is non empty finite set
{{( the scalar of DK . [(Y1 . F),(Y1 . F)]),(p1 .|. p1)},{( the scalar of DK . [(Y1 . F),(Y1 . F)])}} is non empty finite V54() set
addreal . [( the scalar of DK . [(Y1 . F),(Y1 . F)]),(p1 .|. p1)] is set
Z .|. Z is V36() V37() ext-real Element of REAL
addreal . ((Z .|. Z),(p1 .|. p1)) is V36() V37() ext-real Element of REAL
[(Z .|. Z),(p1 .|. p1)] is set
{(Z .|. Z),(p1 .|. p1)} is non empty V43() V44() V45() finite set
{(Z .|. Z)} is non empty V12() V43() V44() V45() finite 1 -element set
{{(Z .|. Z),(p1 .|. p1)},{(Z .|. Z)}} is non empty finite V54() set
addreal . [(Z .|. Z),(p1 .|. p1)] is set
(Z .|. Z) + (Z .|. p1) is V36() V37() ext-real Element of REAL
p1 .|. Z is V36() V37() ext-real Element of REAL
((Z .|. Z) + (Z .|. p1)) + (p1 .|. Z) is V36() V37() ext-real Element of REAL
(((Z .|. Z) + (Z .|. p1)) + (p1 .|. Z)) + (p1 .|. p1) is V36() V37() ext-real Element of REAL
Z + p1 is Element of the carrier of DK
the addF of DK . (Z,p1) is Element of the carrier of DK
the addF of DK . [Z,p1] is set
Z .|. (Z + p1) is V36() V37() ext-real Element of REAL
(Z .|. (Z + p1)) + (p1 .|. Z) is V36() V37() ext-real Element of REAL
((Z .|. (Z + p1)) + (p1 .|. Z)) + (p1 .|. p1) is V36() V37() ext-real Element of REAL
(p1 .|. Z) + (p1 .|. p1) is V36() V37() ext-real Element of REAL
(Z .|. (Z + p1)) + ((p1 .|. Z) + (p1 .|. p1)) is V36() V37() ext-real Element of REAL
p1 .|. (Z + p1) is V36() V37() ext-real Element of REAL
(Z .|. (Z + p1)) + (p1 .|. (Z + p1)) is V36() V37() ext-real Element of REAL
(Z + p1) .|. (Z + p1) is V36() V37() ext-real Element of REAL
the addF of DK . ((Y1 . F),(DX . (F + 1))) is set
[(Y1 . F),(DX . (F + 1))] is set
{(Y1 . F),(DX . (F + 1))} is non empty finite set
{{(Y1 . F),(DX . (F + 1))},{(Y1 . F)}} is non empty finite V54() set
the addF of DK . [(Y1 . F),(DX . (F + 1))] is set
[( the addF of DK . ((Y1 . F),(DX . (F + 1)))),(Z + p1)] is set
{( the addF of DK . ((Y1 . F),(DX . (F + 1)))),(Z + p1)} is non empty finite set
{( the addF of DK . ((Y1 . F),(DX . (F + 1))))} is non empty V12() finite 1 -element set
{{( the addF of DK . ((Y1 . F),(DX . (F + 1)))),(Z + p1)},{( the addF of DK . ((Y1 . F),(DX . (F + 1))))}} is non empty finite V54() set
the scalar of DK . [( the addF of DK . ((Y1 . F),(DX . (F + 1)))),(Z + p1)] is set
Y1 . (F + 1) is set
[( the addF of DK . ((Y1 . F),(DX . (F + 1)))),(Y1 . (F + 1))] is set
{( the addF of DK . ((Y1 . F),(DX . (F + 1)))),(Y1 . (F + 1))} is non empty finite set
{{( the addF of DK . ((Y1 . F),(DX . (F + 1)))),(Y1 . (F + 1))},{( the addF of DK . ((Y1 . F),(DX . (F + 1))))}} is non empty finite V54() set
the scalar of DK . [( the addF of DK . ((Y1 . F),(DX . (F + 1)))),(Y1 . (F + 1))] is set
[(Y1 . (F + 1)),(Y1 . (F + 1))] is set
{(Y1 . (F + 1)),(Y1 . (F + 1))} is non empty finite set
{(Y1 . (F + 1))} is non empty V12() finite 1 -element set
{{(Y1 . (F + 1)),(Y1 . (F + 1))},{(Y1 . (F + 1))}} is non empty finite V54() set
the scalar of DK . [(Y1 . (F + 1)),(Y1 . (F + 1))] is set
Y2 . (F + 1) is set
Y1 . (F + 1) is set
[(Y1 . (F + 1)),(Y1 . (F + 1))] is set
{(Y1 . (F + 1)),(Y1 . (F + 1))} is non empty finite set
{(Y1 . (F + 1))} is non empty V12() finite 1 -element set
{{(Y1 . (F + 1)),(Y1 . (F + 1))},{(Y1 . (F + 1))}} is non empty finite V54() set
the scalar of DK . [(Y1 . (F + 1)),(Y1 . (F + 1))] is set
Y2 . (F + 1) is set
Y1 . (F + 1) is set
[(Y1 . (F + 1)),(Y1 . (F + 1))] is set
{(Y1 . (F + 1)),(Y1 . (F + 1))} is non empty finite set
{(Y1 . (F + 1))} is non empty V12() finite 1 -element set
{{(Y1 . (F + 1)),(Y1 . (F + 1))},{(Y1 . (F + 1))}} is non empty finite V54() set
the scalar of DK . [(Y1 . (F + 1)),(Y1 . (F + 1))] is set
F is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Y2 . F is set
Y1 . F is set
[(Y1 . F),(Y1 . F)] is set
{(Y1 . F),(Y1 . F)} is non empty finite set
{(Y1 . F)} is non empty V12() finite 1 -element set
{{(Y1 . F),(Y1 . F)},{(Y1 . F)}} is non empty finite V54() set
the scalar of DK . [(Y1 . F),(Y1 . F)] is set
F + 1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Y2 . (F + 1) is set
Y1 . (F + 1) is set
[(Y1 . (F + 1)),(Y1 . (F + 1))] is set
{(Y1 . (F + 1)),(Y1 . (F + 1))} is non empty finite set
{(Y1 . (F + 1))} is non empty V12() finite 1 -element set
{{(Y1 . (F + 1)),(Y1 . (F + 1))},{(Y1 . (F + 1))}} is non empty finite V54() set
the scalar of DK . [(Y1 . (F + 1)),(Y1 . (F + 1))] is set

the carrier of DK is non empty set
the scalar of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined REAL -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK),REAL))
K20( the carrier of DK, the carrier of DK) is set
K20(K20( the carrier of DK, the carrier of DK),REAL) is set
K19(K20(K20( the carrier of DK, the carrier of DK),REAL)) is set
the addF of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK))
K20(K20( the carrier of DK, the carrier of DK), the carrier of DK) is set
K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK)) is set
DX is Element of the carrier of DK

len f is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
dom f is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
the addF of DK "**" f is Element of the carrier of DK
DX .|. ( the addF of DK "**" f) is V36() V37() ext-real Element of REAL

dom Y1 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
addreal "**" Y1 is V36() V37() ext-real Element of REAL
K20(NAT, the carrier of DK) is V12() non finite set
K19(K20(NAT, the carrier of DK)) is V12() non finite set
f . 1 is set
Y2 is Relation-like NAT -defined the carrier of DK -valued Function-like non empty V14( NAT ) quasi_total Element of K19(K20(NAT, the carrier of DK))
Y2 . 1 is set
Y2 . (len f) is set
len Y1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Seg (len Y1) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
Seg (len f) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
Y1 . 1 is set

F . 1 is set
F . (len Y1) is set
F . 0 is set
Y2 . 0 is set
[DX,(Y2 . 0)] is set
{DX,(Y2 . 0)} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,(Y2 . 0)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . 0)] is set
Z is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
F . Z is set
Y2 . Z is set
[DX,(Y2 . Z)] is set
{DX,(Y2 . Z)} is non empty finite set
{{DX,(Y2 . Z)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . Z)] is set
Z + 1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
F . (Z + 1) is set
Y2 . (Z + 1) is set
[DX,(Y2 . (Z + 1))] is set
{DX,(Y2 . (Z + 1))} is non empty finite set
{{DX,(Y2 . (Z + 1))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . (Z + 1))] is set
0 + 1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
(len Y1) - 0 is V36() V37() ext-real V41() V42() Element of INT
(Z + 1) - 1 is V36() V37() ext-real V41() V42() Element of INT
dom Y2 is set
rng Y2 is set
f . (Z + 1) is set
rng f is set
F . (Z + 1) is set
Y1 . (Z + 1) is set
addreal . (( the scalar of DK . [DX,(Y2 . Z)]),(Y1 . (Z + 1))) is set
[( the scalar of DK . [DX,(Y2 . Z)]),(Y1 . (Z + 1))] is set
{( the scalar of DK . [DX,(Y2 . Z)]),(Y1 . (Z + 1))} is non empty finite set
{( the scalar of DK . [DX,(Y2 . Z)])} is non empty V12() finite 1 -element set
{{( the scalar of DK . [DX,(Y2 . Z)]),(Y1 . (Z + 1))},{( the scalar of DK . [DX,(Y2 . Z)])}} is non empty finite V54() set
addreal . [( the scalar of DK . [DX,(Y2 . Z)]),(Y1 . (Z + 1))] is set
[DX,(f . (Z + 1))] is set
{DX,(f . (Z + 1))} is non empty finite set
{{DX,(f . (Z + 1))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(f . (Z + 1))] is set
addreal . (( the scalar of DK . [DX,(Y2 . Z)]),( the scalar of DK . [DX,(f . (Z + 1))])) is set
[( the scalar of DK . [DX,(Y2 . Z)]),( the scalar of DK . [DX,(f . (Z + 1))])] is set
{( the scalar of DK . [DX,(Y2 . Z)]),( the scalar of DK . [DX,(f . (Z + 1))])} is non empty finite set
{{( the scalar of DK . [DX,(Y2 . Z)]),( the scalar of DK . [DX,(f . (Z + 1))])},{( the scalar of DK . [DX,(Y2 . Z)])}} is non empty finite V54() set
addreal . [( the scalar of DK . [DX,(Y2 . Z)]),( the scalar of DK . [DX,(f . (Z + 1))])] is set
p2 is Element of the carrier of DK
DX .|. p2 is V36() V37() ext-real Element of REAL
addreal . (( the scalar of DK . [DX,(Y2 . Z)]),(DX .|. p2)) is set
[( the scalar of DK . [DX,(Y2 . Z)]),(DX .|. p2)] is set
{( the scalar of DK . [DX,(Y2 . Z)]),(DX .|. p2)} is non empty finite set
{{( the scalar of DK . [DX,(Y2 . Z)]),(DX .|. p2)},{( the scalar of DK . [DX,(Y2 . Z)])}} is non empty finite V54() set
addreal . [( the scalar of DK . [DX,(Y2 . Z)]),(DX .|. p2)] is set
p1 is Element of the carrier of DK
DX .|. p1 is V36() V37() ext-real Element of REAL
addreal . ((DX .|. p1),(DX .|. p2)) is V36() V37() ext-real Element of REAL
[(DX .|. p1),(DX .|. p2)] is set
{(DX .|. p1),(DX .|. p2)} is non empty V43() V44() V45() finite set
{(DX .|. p1)} is non empty V12() V43() V44() V45() finite 1 -element set
{{(DX .|. p1),(DX .|. p2)},{(DX .|. p1)}} is non empty finite V54() set
addreal . [(DX .|. p1),(DX .|. p2)] is set
(DX .|. p1) + (DX .|. p2) is V36() V37() ext-real Element of REAL
p1 + p2 is Element of the carrier of DK
the addF of DK . (p1,p2) is Element of the carrier of DK
[p1,p2] is set
{p1,p2} is non empty finite set
{p1} is non empty V12() finite 1 -element set
{{p1,p2},{p1}} is non empty finite V54() set
the addF of DK . [p1,p2] is set
DX .|. (p1 + p2) is V36() V37() ext-real Element of REAL
the addF of DK . ((Y2 . Z),(f . (Z + 1))) is set
[(Y2 . Z),(f . (Z + 1))] is set
{(Y2 . Z),(f . (Z + 1))} is non empty finite set
{(Y2 . Z)} is non empty V12() finite 1 -element set
{{(Y2 . Z),(f . (Z + 1))},{(Y2 . Z)}} is non empty finite V54() set
the addF of DK . [(Y2 . Z),(f . (Z + 1))] is set
[DX,( the addF of DK . ((Y2 . Z),(f . (Z + 1))))] is set
{DX,( the addF of DK . ((Y2 . Z),(f . (Z + 1))))} is non empty finite set
{{DX,( the addF of DK . ((Y2 . Z),(f . (Z + 1))))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,( the addF of DK . ((Y2 . Z),(f . (Z + 1))))] is set
Y2 . (Z + 1) is set
[DX,(Y2 . (Z + 1))] is set
{DX,(Y2 . (Z + 1))} is non empty finite set
{{DX,(Y2 . (Z + 1))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . (Z + 1))] is set
F . (Z + 1) is set
Y2 . (Z + 1) is set
[DX,(Y2 . (Z + 1))] is set
{DX,(Y2 . (Z + 1))} is non empty finite set
{{DX,(Y2 . (Z + 1))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . (Z + 1))] is set
F . (Z + 1) is set
Y2 . (Z + 1) is set
[DX,(Y2 . (Z + 1))] is set
{DX,(Y2 . (Z + 1))} is non empty finite set
{{DX,(Y2 . (Z + 1))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . (Z + 1))] is set
Z is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
F . Z is set
Y2 . Z is set
[DX,(Y2 . Z)] is set
{DX,(Y2 . Z)} is non empty finite set
{{DX,(Y2 . Z)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . Z)] is set
Z + 1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
F . (Z + 1) is set
Y2 . (Z + 1) is set
[DX,(Y2 . (Z + 1))] is set
{DX,(Y2 . (Z + 1))} is non empty finite set
{{DX,(Y2 . (Z + 1))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . (Z + 1))] is set
Y2 . (len Y1) is set
[DX,(Y2 . (len Y1))] is set
{DX,(Y2 . (len Y1))} is non empty finite set
{{DX,(Y2 . (len Y1))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . (len Y1))] is set
[DX,(Y2 . (len f))] is set
{DX,(Y2 . (len f))} is non empty finite set
{{DX,(Y2 . (len f))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . (len f))] is set

the carrier of DK is non empty set
K19( the carrier of DK) is set
K20( the carrier of DK, the carrier of DK) is set
K19(K20( the carrier of DK, the carrier of DK)) is set
the scalar of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined REAL -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK),REAL))
K20(K20( the carrier of DK, the carrier of DK),REAL) is set
K19(K20(K20( the carrier of DK, the carrier of DK),REAL)) is set
K20( the carrier of DK,REAL) is V12() non finite set
K19(K20( the carrier of DK,REAL)) is V12() non finite set
the addF of DK is Relation-like K20( the carrier of DK, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20( the carrier of DK, the carrier of DK)) quasi_total Element of K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK))
K20(K20( the carrier of DK, the carrier of DK), the carrier of DK) is set
K19(K20(K20( the carrier of DK, the carrier of DK), the carrier of DK)) is set
DX is non empty finite Element of K19( the carrier of DK)
f is Relation-like the carrier of DK -defined the carrier of DK -valued Function-like non empty V14( the carrier of DK) quasi_total Element of K19(K20( the carrier of DK, the carrier of DK))
dom f is set
Y1 is Relation-like the carrier of DK -defined REAL -valued Function-like non empty V14( the carrier of DK) quasi_total Element of K19(K20( the carrier of DK,REAL))
dom Y1 is set
Y2 is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK
rng Y2 is set
( the carrier of DK, the carrier of DK,f,Y2) is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK

the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2) is Element of the carrier of DK
[( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2)),( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2))] is set
{( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2)),( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2))} is non empty finite set
{( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2))} is non empty V12() finite 1 -element set
{{( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2)),( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2))},{( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2))}} is non empty finite V54() set
the scalar of DK . [( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2)),( the addF of DK "**" ( the carrier of DK, the carrier of DK,f,Y2))] is set

addreal "**" (REAL, the carrier of DK,Y1,Y2) is V36() V37() ext-real Element of REAL
p1 is set
dom Y2 is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
Y2 . p1 is set
dom ( the carrier of DK, the carrier of DK,f,Y2) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
len Y2 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Seg (len Y2) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
len ( the carrier of DK, the carrier of DK,f,Y2) is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
Seg (len ( the carrier of DK, the carrier of DK,f,Y2)) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
card DX is non empty V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
0 + 1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
p1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
( the carrier of DK, the carrier of DK,f,Y2) . p1 is set
p2 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
( the carrier of DK, the carrier of DK,f,Y2) . p2 is set
[(( the carrier of DK, the carrier of DK,f,Y2) . p1),(( the carrier of DK, the carrier of DK,f,Y2) . p2)] is set
{(( the carrier of DK, the carrier of DK,f,Y2) . p1),(( the carrier of DK, the carrier of DK,f,Y2) . p2)} is non empty finite set
{(( the carrier of DK, the carrier of DK,f,Y2) . p1)} is non empty V12() finite 1 -element set
{{(( the carrier of DK, the carrier of DK,f,Y2) . p1),(( the carrier of DK, the carrier of DK,f,Y2) . p2)},{(( the carrier of DK, the carrier of DK,f,Y2) . p1)}} is non empty finite V54() set
the scalar of DK . [(( the carrier of DK, the carrier of DK,f,Y2) . p1),(( the carrier of DK, the carrier of DK,f,Y2) . p2)] is set
Y2 . p1 is set
Y2 . p2 is set