let
T
be non
empty
TopStruct
;
:: thesis:
for
c
being
Curve
of
T
holds
Sum
<*
c
*>
=
c
let
c
be
Curve
of
T
;
:: thesis:
Sum
<*
c
*>
=
c
set
f
=
<*
c
*>
;
len
<*
c
*>
=
1
by
FINSEQ_1:40
;
hence
Sum
<*
c
*>
=
(
Partial_Sums
<*
c
*>
)
.
1
by
Def14
.=
<*
c
*>
.
1
by
Def13
.=
c
by
FINSEQ_1:40
;
:: thesis:
verum