theorem
Th4
:
:: BHSP_6:4
for
X
being
RealUnitarySpace
for
L
being
linear-Functional
of
X
for
p
being
FinSequence
of the
carrier
of
X
st
len
p
>=
1 holds
for
q
being
FinSequence
of
REAL
st
dom
p
=
dom
q
& ( for
i
being
Nat
st
i
in
dom
q
holds
q
.
i
=
L
.
(
p
.
i
)
) holds
L
.
(
the
addF
of
X
"**"
p
)
=
addreal
"**"
q