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 ;
:: thesis: verum