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

addreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V14(K20(REAL,REAL)) quasi_total commutative associative having_a_unity Element of K19(K20(K20(REAL,REAL),REAL))

DK is set

DX is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

f is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

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

DX " is Relation-like Function-like 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)

Y1 is Relation-like Function-like FinSequence-like set

rng Y1 is set

Y2 is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

DX "**" Y2 is Element of DK

F is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

rng F is set

DX "**" F is Element of DK

Y1 is Element of DK

Y2 is Element of DK

F is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

rng F is set

DX "**" F is Element of DK

F is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

rng F is set

DX "**" F is Element of DK

Z is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK

rng Z is set

DX "**" Z is Element of DK

Z is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence 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

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

p1 * F is Relation-like Function-like set

dom p1 is set

rng p1 is set

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

f is Relation-like Function-like FinSequence-like set

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

Y1 is Relation-like NAT -defined DX -valued Function-like FinSequence-like FinSequence of DX

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

Y1 * f is Relation-like Function-like 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

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

F is Relation-like Function-like FinSequence-like set

rng F is set

Z is Relation-like NAT -defined DX -valued Function-like FinSequence-like FinSequence of DX

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

Z * Y2 is Relation-like Function-like set

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

p1 is Relation-like NAT -defined DX -valued Function-like FinSequence-like FinSequence of DX

rng p1 is set

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

p1 * Y2 is Relation-like Function-like set

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

F is Element of DK

Z is Element of DK

p1 is Relation-like NAT -defined DX -valued Function-like FinSequence-like FinSequence of DX

rng p1 is set

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

p1 * Y2 is Relation-like Function-like set

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

p1 is Relation-like NAT -defined DX -valued Function-like FinSequence-like FinSequence of DX

rng p1 is set

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

p1 * Y2 is Relation-like Function-like set

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

p2 is Relation-like NAT -defined DX -valued Function-like FinSequence-like FinSequence of DX

rng p2 is set

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

p2 * Y2 is Relation-like Function-like set

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

p2 is Relation-like NAT -defined DX -valued Function-like FinSequence-like FinSequence of DX

rng p2 is set

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

p2 * Y2 is Relation-like Function-like set

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

q * p1 is Relation-like Function-like set

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

Y1 is Relation-like Function-like FinSequence-like set

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

Z is Relation-like Function-like FinSequence-like set

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

p1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence 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

F is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK

rng F is set

Z is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

F is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK

rng F is set

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

Z is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK

rng Z is set

p1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

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

Z is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK

rng Z is set

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

p1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence 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

p1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence 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

p2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence 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

p2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence 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

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

q * F is Relation-like Function-like set

dom q is set

rng q is set

s is set

q . s is set

q * p1 is Relation-like Function-like 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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of DK is non empty set

K19( the carrier of DK) is set

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of DK is non empty set

K19( the carrier of DK) is set

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

||.f.|| is V36() V37() ext-real Element of REAL

||.f.|| ^2 is V36() V37() ext-real Element of REAL

K143(||.f.||,||.f.||) is set

2 * (||.f.|| ^2) is V36() V37() ext-real Element of REAL

(2 * (||.DX.|| ^2)) + (2 * (||.f.|| ^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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

||.f.|| is V36() V37() ext-real Element of REAL

||.f.|| ^2 is V36() V37() ext-real Element of REAL

K143(||.f.||,||.f.||) is set

(||.DX.|| ^2) + (||.f.|| ^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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

f is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence 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 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total Element of K19(K20(NAT,REAL))

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

f is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence 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

Y1 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence 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 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total Element of K19(K20(NAT,REAL))

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

DK is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

Y2 * f is Relation-like Function-like set

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

(REAL, the carrier of DK,Y1,Y2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL

Y2 * Y1 is Relation-like Function-like 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