:: 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
f . (Y2 . p1) is set
f . (Y2 . p2) is set
p1 is set
Y2 . p1 is set
dom (REAL, the carrier of DK,Y1,Y2) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
p1 is V29() V30() V31() V35() V36() V37() ext-real V41() V42() V43() V44() V45() V46() V47() V48() finite cardinal Element of NAT
(REAL, the carrier of DK,Y1,Y2) . p1 is set
( the carrier of DK, the carrier of DK,f,Y2) . p1 is set
[(( the carrier of DK, the carrier of DK,f,Y2) . p1),(( the carrier of DK, the carrier of DK,f,Y2) . p1)] is set
{(( the carrier of DK, the carrier of DK,f,Y2) . p1),(( the carrier of DK, the carrier of DK,f,Y2) . p1)} 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) . p1)},{(( 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) . p1)] is set
Y2 . p1 is set
Y1 . (Y2 . p1) is set
f . (Y2 . p1) is set
[(f . (Y2 . p1)),(f . (Y2 . p1))] is set
{(f . (Y2 . p1)),(f . (Y2 . p1))} is non empty finite set
{(f . (Y2 . p1))} is non empty V12() finite 1 -element set
{{(f . (Y2 . p1)),(f . (Y2 . p1))},{(f . (Y2 . p1))}} is non empty finite V54() set
the scalar of DK . [(f . (Y2 . p1)),(f . (Y2 . p1))] is set
(Y2 * f) . p1 is set
[((Y2 * f) . p1),(f . (Y2 . p1))] is set
{((Y2 * f) . p1),(f . (Y2 . p1))} is non empty finite set
{((Y2 * f) . p1)} is non empty V12() finite 1 -element set
{{((Y2 * f) . p1),(f . (Y2 . p1))},{((Y2 * f) . p1)}} is non empty finite V54() set
the scalar of DK . [((Y2 * f) . p1),(f . (Y2 . p1))] 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 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
K20( the carrier of DK, the carrier of DK) is set
K19(K20( the carrier of DK, the carrier of DK)) 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 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
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 non empty finite Element of K19( the carrier of DK)
Y1 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 Y1 is set
Y2 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 Y2 is set
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
( the carrier of DK, the carrier of DK,Y1,F) is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK
F * Y1 is Relation-like Function-like set
the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F) is Element of the carrier of DK
[DX,( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))] is set
{DX,( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))] is set
(REAL, the carrier of DK,Y2,F) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
F * Y2 is Relation-like Function-like set
addreal "**" (REAL, the carrier of DK,Y2,F) is V36() V37() ext-real Element of REAL
p2 is set
dom F is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
F . p2 is set
dom ( the carrier of DK, the carrier of DK,Y1,F) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
p2 is set
F . p2 is set
dom (REAL, the carrier of DK,Y2,F) 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
(REAL, the carrier of DK,Y2,F) . p2 is set
( the carrier of DK, the carrier of DK,Y1,F) . p2 is set
[DX,(( the carrier of DK, the carrier of DK,Y1,F) . p2)] is set
{DX,(( the carrier of DK, the carrier of DK,Y1,F) . p2)} is non empty finite set
{{DX,(( the carrier of DK, the carrier of DK,Y1,F) . p2)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(( the carrier of DK, the carrier of DK,Y1,F) . p2)] is set
F . p2 is set
Y2 . (F . p2) is set
Y1 . (F . p2) is set
[DX,(Y1 . (F . p2))] is set
{DX,(Y1 . (F . p2))} is non empty finite set
{{DX,(Y1 . (F . p2))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y1 . (F . p2))] 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)
len ( the carrier of DK, the carrier of DK,Y1,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 ( the carrier of DK, the carrier of DK,Y1,F)) is V43() V44() V45() V46() V47() V48() Element of K19(NAT)
card f 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
DX .|. ( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,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
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
K20( the carrier of DK,REAL) is V12() non finite set
K19(K20( the carrier of DK,REAL)) is V12() non finite set
K19(K20( the carrier of DK, the carrier of DK)) is set
DX is Element of the carrier of DK
f is finite (DK)
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
(REAL, the carrier of DK,addreal,f,Y1) is V36() V37() ext-real Element of REAL
Y2 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 Y2 is set
( the carrier of DK, the carrier of DK, the addF of DK,f,Y2) is Element of the carrier of DK
DX .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,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
( the carrier of DK, the carrier of DK,Y2,F) is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK
F * Y2 is Relation-like Function-like set
the addF of DK "**" ( the carrier of DK, the carrier of DK,Y2,F) is Element of the carrier of DK
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
Z is Element of the carrier of DK
Y1 . Z is set
Y2 . Z is set
[DX,(Y2 . Z)] is set
{DX,(Y2 . Z)} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,(Y2 . Z)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,(Y2 . Z)] is set
DX .|. Z is V36() V37() ext-real Element of REAL
(DX .|. Z) ^2 is V36() V37() ext-real Element of REAL
K143((DX .|. Z),(DX .|. Z)) is set
(DX .|. Z) * Z is Element of the carrier of DK
the Mult of DK is Relation-like K20(REAL, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20(REAL, the carrier of DK)) quasi_total Element of K19(K20(K20(REAL, the carrier of DK), the carrier of DK))
K20(REAL, the carrier of DK) is V12() non finite set
K20(K20(REAL, the carrier of DK), the carrier of DK) is V12() non finite set
K19(K20(K20(REAL, the carrier of DK), the carrier of DK)) is V12() non finite set
the Mult of DK . ((DX .|. Z),Z) is set
[(DX .|. Z),Z] is set
{(DX .|. Z),Z} is non empty finite set
{(DX .|. Z)} is non empty V12() V43() V44() V45() finite 1 -element set
{{(DX .|. Z),Z},{(DX .|. Z)}} is non empty finite V54() set
the Mult of DK . [(DX .|. Z),Z] is set
DX .|. ((DX .|. Z) * Z) is V36() V37() ext-real Element of REAL
[DX,((DX .|. Z) * Z)] is set
{DX,((DX .|. Z) * Z)} is non empty finite set
{{DX,((DX .|. Z) * Z)},{DX}} is non empty finite V54() set
the scalar of DK . [DX,((DX .|. Z) * Z)] is set
(REAL, the carrier of DK,Y1,F) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
F * Y1 is Relation-like Function-like set
addreal "**" (REAL, the carrier of DK,Y1,F) is V36() V37() ext-real Element of REAL
[DX,( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y2,F))] is set
{DX,( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y2,F))} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y2,F))},{DX}} is non empty finite V54() set
the scalar of DK . [DX,( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y2,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
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
K19(K20( the carrier of DK, the carrier of DK)) 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
DX is Element of the carrier of DK
f is finite (DK)
Y1 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 Y1 is set
( the carrier of DK, the carrier of DK, the addF of DK,f,Y1) is Element of the carrier of DK
( the carrier of DK, the carrier of DK, the addF of DK,f,Y1) .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,Y1) is V36() V37() ext-real Element of REAL
Y2 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 Y2 is set
(REAL, the carrier of DK,addreal,f,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
( the carrier of DK, the carrier of DK,Y1,F) is Relation-like NAT -defined the carrier of DK -valued Function-like FinSequence-like FinSequence of the carrier of DK
F * Y1 is Relation-like Function-like set
the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F) is Element of the carrier of DK
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
Z is Element of the carrier of DK
Y1 . Z is set
p1 is Element of the carrier of DK
Y1 . p1 is set
[(Y1 . Z),(Y1 . p1)] is set
{(Y1 . Z),(Y1 . p1)} is non empty finite set
{(Y1 . Z)} is non empty V12() finite 1 -element set
{{(Y1 . Z),(Y1 . p1)},{(Y1 . Z)}} is non empty finite V54() set
the scalar of DK . [(Y1 . Z),(Y1 . p1)] is set
DX .|. Z is V36() V37() ext-real Element of REAL
DX .|. p1 is V36() V37() ext-real Element of REAL
Z .|. p1 is V36() V37() ext-real Element of REAL
(DX .|. Z) * Z is Element of the carrier of DK
the Mult of DK is Relation-like K20(REAL, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20(REAL, the carrier of DK)) quasi_total Element of K19(K20(K20(REAL, the carrier of DK), the carrier of DK))
K20(REAL, the carrier of DK) is V12() non finite set
K20(K20(REAL, the carrier of DK), the carrier of DK) is V12() non finite set
K19(K20(K20(REAL, the carrier of DK), the carrier of DK)) is V12() non finite set
the Mult of DK . ((DX .|. Z),Z) is set
[(DX .|. Z),Z] is set
{(DX .|. Z),Z} is non empty finite set
{(DX .|. Z)} is non empty V12() V43() V44() V45() finite 1 -element set
{{(DX .|. Z),Z},{(DX .|. Z)}} is non empty finite V54() set
the Mult of DK . [(DX .|. Z),Z] is set
[((DX .|. Z) * Z),(Y1 . p1)] is set
{((DX .|. Z) * Z),(Y1 . p1)} is non empty finite set
{((DX .|. Z) * Z)} is non empty V12() finite 1 -element set
{{((DX .|. Z) * Z),(Y1 . p1)},{((DX .|. Z) * Z)}} is non empty finite V54() set
the scalar of DK . [((DX .|. Z) * Z),(Y1 . p1)] is set
(DX .|. p1) * p1 is Element of the carrier of DK
the Mult of DK . ((DX .|. p1),p1) is set
[(DX .|. p1),p1] is set
{(DX .|. p1),p1} is non empty finite set
{(DX .|. p1)} is non empty V12() V43() V44() V45() finite 1 -element set
{{(DX .|. p1),p1},{(DX .|. p1)}} is non empty finite V54() set
the Mult of DK . [(DX .|. p1),p1] is set
[((DX .|. Z) * Z),((DX .|. p1) * p1)] is set
{((DX .|. Z) * Z),((DX .|. p1) * p1)} is non empty finite set
{{((DX .|. Z) * Z),((DX .|. p1) * p1)},{((DX .|. Z) * Z)}} is non empty finite V54() set
the scalar of DK . [((DX .|. Z) * Z),((DX .|. p1) * p1)] is set
((DX .|. Z) * Z) .|. ((DX .|. p1) * p1) is V36() V37() ext-real Element of REAL
p1 .|. ((DX .|. Z) * Z) is V36() V37() ext-real Element of REAL
(DX .|. p1) * (p1 .|. ((DX .|. Z) * Z)) is V36() V37() ext-real Element of REAL
p1 .|. Z is V36() V37() ext-real Element of REAL
(DX .|. Z) * (p1 .|. Z) is V36() V37() ext-real Element of REAL
(DX .|. p1) * ((DX .|. Z) * (p1 .|. Z)) is V36() V37() ext-real Element of REAL
Z is Element of the carrier of DK
Y2 . Z is set
Y1 . Z is set
[(Y1 . Z),(Y1 . Z)] is set
{(Y1 . Z),(Y1 . Z)} is non empty finite set
{(Y1 . Z)} is non empty V12() finite 1 -element set
{{(Y1 . Z),(Y1 . Z)},{(Y1 . Z)}} is non empty finite V54() set
the scalar of DK . [(Y1 . Z),(Y1 . Z)] is set
DX .|. Z is V36() V37() ext-real Element of REAL
(DX .|. Z) * Z is Element of the carrier of DK
the Mult of DK is Relation-like K20(REAL, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20(REAL, the carrier of DK)) quasi_total Element of K19(K20(K20(REAL, the carrier of DK), the carrier of DK))
K20(REAL, the carrier of DK) is V12() non finite set
K20(K20(REAL, the carrier of DK), the carrier of DK) is V12() non finite set
K19(K20(K20(REAL, the carrier of DK), the carrier of DK)) is V12() non finite set
the Mult of DK . ((DX .|. Z),Z) is set
[(DX .|. Z),Z] is set
{(DX .|. Z),Z} is non empty finite set
{(DX .|. Z)} is non empty V12() V43() V44() V45() finite 1 -element set
{{(DX .|. Z),Z},{(DX .|. Z)}} is non empty finite V54() set
the Mult of DK . [(DX .|. Z),Z] is set
(DX .|. Z) ^2 is V36() V37() ext-real Element of REAL
K143((DX .|. Z),(DX .|. Z)) is set
(DX .|. Z) * (DX .|. Z) is V36() V37() ext-real Element of REAL
((DX .|. Z) * (DX .|. Z)) * 1 is V36() V37() ext-real Element of REAL
Z .|. Z is V36() V37() ext-real Element of REAL
((DX .|. Z) * (DX .|. Z)) * (Z .|. Z) is V36() V37() ext-real Element of REAL
(DX .|. Z) * (Z .|. Z) is V36() V37() ext-real Element of REAL
(DX .|. Z) * ((DX .|. Z) * (Z .|. Z)) is V36() V37() ext-real Element of REAL
((DX .|. Z) * Z) .|. Z is V36() V37() ext-real Element of REAL
(DX .|. Z) * (((DX .|. Z) * Z) .|. Z) is V36() V37() ext-real Element of REAL
((DX .|. Z) * Z) .|. ((DX .|. Z) * Z) is V36() V37() ext-real Element of REAL
[( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F)),( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))] is set
{( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F)),( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))} is non empty finite set
{( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))} is non empty V12() finite 1 -element set
{{( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F)),( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))},{( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))}} is non empty finite V54() set
the scalar of DK . [( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F)),( the addF of DK "**" ( the carrier of DK, the carrier of DK,Y1,F))] is set
(REAL, the carrier of DK,Y2,F) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like FinSequence of REAL
F * Y2 is Relation-like Function-like set
addreal "**" (REAL, the carrier of DK,Y2,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
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
K20( the carrier of DK,REAL) is V12() non finite set
K19(K20( the carrier of DK,REAL)) is V12() non finite 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 finite (DK)
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
(REAL, the carrier of DK,addreal,f,Y1) is V36() V37() ext-real Element of REAL
the Mult of DK is Relation-like K20(REAL, the carrier of DK) -defined the carrier of DK -valued Function-like V14(K20(REAL, the carrier of DK)) quasi_total Element of K19(K20(K20(REAL, the carrier of DK), the carrier of DK))
K20(REAL, the carrier of DK) is V12() non finite set
K20(K20(REAL, the carrier of DK), the carrier of DK) is V12() non finite set
K19(K20(K20(REAL, the carrier of DK), the carrier of DK)) is V12() non finite 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
Y2 is set
[DX,Y2] is set
{DX,Y2} is non empty finite set
{DX} is non empty V12() finite 1 -element set
{{DX,Y2},{DX}} is non empty finite V54() set
the scalar of DK . [DX,Y2] is set
[( the scalar of DK . [DX,Y2]),Y2] is set
{( the scalar of DK . [DX,Y2]),Y2} is non empty finite set
{( the scalar of DK . [DX,Y2])} is non empty V12() finite 1 -element set
{{( the scalar of DK . [DX,Y2]),Y2},{( the scalar of DK . [DX,Y2])}} is non empty finite V54() set
the Mult of DK . [( the scalar of DK . [DX,Y2]),Y2] is set
F is Element of the carrier of DK
DX .|. F is V36() V37() ext-real Element of REAL
the Mult of DK . (( the scalar of DK . [DX,Y2]),Y2) is set
p2 is Element of the carrier of DK
p1 is V36() V37() ext-real Element of REAL
p1 * p2 is Element of the carrier of DK
the Mult of DK . (p1,p2) is set
[p1,p2] is set
{p1,p2} is non empty finite set
{p1} is non empty V12() V43() V44() V45() finite 1 -element set
{{p1,p2},{p1}} is non empty finite V54() set
the Mult of DK . [p1,p2] is set
K19(K20( the carrier of DK, the carrier of DK)) is set
Y2 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))
Y2 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 Y2 is set
F is Element of the carrier of DK
Y2 . F is set
[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 scalar of DK . [DX,F] is set
[( the scalar of DK . [DX,F]),F] is set
{( the scalar of DK . [DX,F]),F} is non empty finite set
{( the scalar of DK . [DX,F])} is non empty V12() finite 1 -element set
{{( the scalar of DK . [DX,F]),F},{( the scalar of DK . [DX,F])}} is non empty finite V54() set
the Mult of DK . [( the scalar of DK . [DX,F]),F] is set
DX .|. F is V36() V37() ext-real Element of REAL
(DX .|. F) * F is Element of the carrier of DK
the Mult of DK . ((DX .|. F),F) is set
[(DX .|. F),F] is set
{(DX .|. F),F} is non empty finite set
{(DX .|. F)} is non empty V12() V43() V44() V45() finite 1 -element set
{{(DX .|. F),F},{(DX .|. F)}} is non empty finite V54() set
the Mult of DK . [(DX .|. F),F] is set
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
( the carrier of DK, the carrier of DK, the addF of DK,f,F) is Element of the carrier of DK
( the carrier of DK, the carrier of DK, the addF of DK,f,F) .|. DX is V36() V37() ext-real Element of REAL
DX .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,F) is V36() V37() ext-real Element of REAL
( the carrier of DK, the carrier of DK, the addF of DK,f,F) .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,F) is V36() V37() ext-real Element of REAL
DX - ( the carrier of DK, the carrier of DK, the addF of DK,f,F) is Element of the carrier of DK
- ( the carrier of DK, the carrier of DK, the addF of DK,f,F) is Element of the carrier of DK
DX + (- ( the carrier of DK, the carrier of DK, the addF of DK,f,F)) is Element of the carrier of DK
the addF of DK . (DX,(- ( the carrier of DK, the carrier of DK, the addF of DK,f,F))) is Element of the carrier of DK
[DX,(- ( the carrier of DK, the carrier of DK, the addF of DK,f,F))] is set
{DX,(- ( the carrier of DK, the carrier of DK, the addF of DK,f,F))} is non empty finite set
{{DX,(- ( the carrier of DK, the carrier of DK, the addF of DK,f,F))},{DX}} is non empty finite V54() set
the addF of DK . [DX,(- ( the carrier of DK, the carrier of DK, the addF of DK,f,F))] is set
(DX - ( the carrier of DK, the carrier of DK, the addF of DK,f,F)) .|. (DX - ( the carrier of DK, the carrier of DK, the addF of DK,f,F)) is V36() V37() ext-real Element of REAL
DX .|. DX is V36() V37() ext-real Element of REAL
(DX .|. DX) - (( the carrier of DK, the carrier of DK, the addF of DK,f,F) .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,F)) is V36() V37() ext-real Element of REAL
((DX .|. DX) - (( the carrier of DK, the carrier of DK, the addF of DK,f,F) .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,F))) - (( the carrier of DK, the carrier of DK, the addF of DK,f,F) .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,F)) is V36() V37() ext-real Element of REAL
(((DX .|. DX) - (( the carrier of DK, the carrier of DK, the addF of DK,f,F) .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,F))) - (( the carrier of DK, the carrier of DK, the addF of DK,f,F) .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,F))) + (( the carrier of DK, the carrier of DK, the addF of DK,f,F) .|. ( the carrier of DK, the carrier of DK, the addF of DK,f,F)) is V36() V37() ext-real Element of REAL
(DX .|. DX) - (REAL, the carrier of DK,addreal,f,Y1) is V36() V37() ext-real Element of REAL
0 + (REAL, the carrier of DK,addreal,f,Y1) 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
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 non empty set
K19(DX) is set
K20(DX,DK) is set
K19(K20(DX,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))
Y1 is finite Element of K19(DX)
Y2 is finite Element of K19(DX)
Y1 \/ Y2 is finite set
F is Relation-like DX -defined DK -valued Function-like non empty V14(DX) quasi_total Element of K19(K20(DX,DK))
dom F is set
(DK,DX,f,Y1,F) is Element of DK
(DK,DX,f,Y2,F) is Element of DK
f . ((DK,DX,f,Y1,F),(DK,DX,f,Y2,F)) is Element of DK
[(DK,DX,f,Y1,F),(DK,DX,f,Y2,F)] is set
{(DK,DX,f,Y1,F),(DK,DX,f,Y2,F)} is non empty finite set
{(DK,DX,f,Y1,F)} is non empty V12() finite 1 -element set
{{(DK,DX,f,Y1,F),(DK,DX,f,Y2,F)},{(DK,DX,f,Y1,F)}} is non empty finite V54() set
f . [(DK,DX,f,Y1,F),(DK,DX,f,Y2,F)] is set
Z is finite Element of K19(DX)
(DK,DX,f,Z,F) 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,F,p1) is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK
p1 * F is Relation-like Function-like set
f "**" (DK,DX,F,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,F,p2) is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK
p2 * F is Relation-like Function-like set
f "**" (DK,DX,F,p2) is Element of DK
p1 ^ p2 is Relation-like NAT -defined DX -valued Function-like FinSequence-like FinSequence of DX
rng (p1 ^ p2) is set
(DK,DX,F,(p1 ^ p2)) is Relation-like NAT -defined DK -valued Function-like FinSequence-like FinSequence of DK
(p1 ^ p2) * F is Relation-like Function-like set
f "**" (DK,DX,F,(p1 ^ p2)) is Element of DK
s is Relation-like Function-like FinSequence-like set
t is Relation-like Function-like FinSequence-like set
s ^ t is Relation-like Function-like FinSequence-like set