let T be non empty TopStruct ; :: thesis: for c being Curve of T
for f being FinSequence of Curves T holds Sum (f ^ <*c*>) = (Sum f) + c
let c be Curve of T; :: thesis: for f being FinSequence of Curves T holds Sum (f ^ <*c*>) = (Sum f) + c
let f be FinSequence of Curves T; :: thesis: Sum (f ^ <*c*>) = (Sum f) + c

per cases ( len f <= 0 or len f > 0 ) ;

suppose A1: len f <= 0 ; :: thesis: Sum (f ^ <*c*>) = (Sum f) + c

A2: f = {} by A1;
reconsider c0 = {} as Curve of T by Th21;
thus Sum (f ^ <*c*>) = Sum <*c*> by A2, FINSEQ_1:34
.= c0 \/ c by Th40
.= c0 + c by Def12
.= (Sum f) + c by Def14, A1 ; :: thesis: verum

end;

suppose A3: len f > 0 ; :: thesis: Sum (f ^ <*c*>) = (Sum f) + c

set f1 = f ^ <*c*>;
A4: len (f ^ <*c*>) = (len f) + (len <*c*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
A5: Sum (f ^ <*c*>) = (Partial_Sums (f ^ <*c*>)) . (len (f ^ <*c*>)) by Def14;
0 < 0 + (len f) by A3;
then A6: 1 <= len f by NAT_1:19;
A7: len f < len (f ^ <*c*>) by A4, NAT_1:13;
len f in Seg (len (f ^ <*c*>)) by A6, A7, FINSEQ_1:1;
then len f in Seg (len (Partial_Sums (f ^ <*c*>))) by Def13;
then len f in dom (Partial_Sums (f ^ <*c*>)) by FINSEQ_1:def 3;
then A8: (Partial_Sums (f ^ <*c*>)) /. (len f) = (Partial_Sums (f ^ <*c*>)) . (len f) by PARTFUN1:def 6
.= (Partial_Sums f) . (len f) by Lm2
.= Sum f by A3, Def14 ;
len (f ^ <*c*>) in Seg (len (f ^ <*c*>)) by FINSEQ_1:3;
then len (f ^ <*c*>) in dom (f ^ <*c*>) by FINSEQ_1:def 3;
then A9: (f ^ <*c*>) /. ((len f) + 1) = (f ^ <*c*>) . ((len f) + 1) by A4, PARTFUN1:def 6
.= c by FINSEQ_1:42 ;
thus Sum (f ^ <*c*>) = (Sum f) + c by A8, A9, A5, A7, A4, A6, Def13; :: thesis: verum

end;

end;