reconsider
F
=
<*>
ExtREAL
as
FinSequence
of
ExtREAL
;
ex
f
being
sequence
of
ExtREAL
st
(
Sum
F
=
f
.
(
len
F
)
&
f
.
0
=
0.
& ( for
i
being
Nat
st
i
<
len
F
holds
f
.
(
i
+
1
)
=
(
f
.
i
)
+
(
F
.
(
i
+
1
)
)
) )
by
Def2
;
hence
Sum
(
<*>
ExtREAL
)
=
0.
;
:: thesis:
verum