let m be non zero Nat; :: thesis: for s, s1 being FinSequence of REAL m
for s0 being Element of REAL m st s1 = s ^ <*s0*> holds
Sum s1 = (Sum s) + s0
let s, s1 be FinSequence of REAL m; :: thesis: for s0 being Element of REAL m st s1 = s ^ <*s0*> holds
Sum s1 = (Sum s) + s0
let s0 be Element of REAL m; :: thesis: ( s1 = s ^ <*s0*> implies Sum s1 = (Sum s) + s0 )
assume A1: s1 = s ^ <*s0*> ; :: thesis: Sum s1 = (Sum s) + s0
dom s = Seg (len s) by FINSEQ_1:def 3;
then A2: s = s1 | (len s) by A1, FINSEQ_1:21;

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

suppose A3: len s = 0 ; :: thesis: Sum s1 = (Sum s) + s0

then s = {} ;
then A4: s1 = <*s0*> by A1, FINSEQ_1:34;
len s1 = (len s) + (len <*s0*>) by A1, FINSEQ_1:22
.= 0 + 1 by A3, FINSEQ_1:40 ;
then A6: Sum s1 = (accum s1) . 1 by EUCLID_7:def 11
.= s1 . 1 by EUCLID_7:def 10
.= s0 by A4 ;
Sum s = 0* m by A3, EUCLID_7:def 11;
hence Sum s1 = (Sum s) + s0 by A6, EUCLID_4:1; :: thesis: verum

end;

suppose A7: len s <> 0 ; :: thesis: Sum s1 = (Sum s) + s0

then A8: 1 <= len s by NAT_1:14;
then len s in Seg (len s) ;
then len s in Seg (len (accum s)) by EUCLID_7:def 10;
then A9: len s in dom (accum s) by FINSEQ_1:def 3;
A10: len s1 = (len s) + (len <*s0*>) by A1, FINSEQ_1:22
.= (len s) + 1 by FINSEQ_1:40 ;
A11: len s < len s1 by A10, NAT_1:13;
then len s in Seg (len s1) by A8;
then len s in Seg (len (accum s1)) by EUCLID_7:def 10;
then len s in dom (accum s1) by FINSEQ_1:def 3;
then A13: (accum s1) /. (len s) = (accum s1) . (len s) by PARTFUN1:def 6
.= (accum s) . (len s) by A2, A8, Th2
.= (accum s) /. (len s) by A9, PARTFUN1:def 6 ;
A14: (accum s) /. (len s) = (accum s) . (len s) by A9, PARTFUN1:def 6
.= Sum s by A7, EUCLID_7:def 11 ;
(len s) + 1 in Seg (len s1) by A10, FINSEQ_1:4;
then (len s) + 1 in dom s1 by FINSEQ_1:def 3;
then A15: s1 /. ((len s) + 1) = s1 . ((len s) + 1) by PARTFUN1:def 6
.= s0 by A1, FINSEQ_1:42 ;
thus Sum s1 = (accum s1) . ((len s) + 1) by A10, EUCLID_7:def 11
.= (Sum s) + s0 by A7, A11, A13, A14, A15, NAT_1:14, EUCLID_7:def 10 ; :: thesis: verum

end;

end;