let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for f, g being FinSequence of the carrier of L
for n being Nat st len f = n + 1 & g = f | (Seg n) holds
Sum f = (Sum g) + (f /. (len f))
let f, g be FinSequence of the carrier of L; :: thesis: for n being Nat st len f = n + 1 & g = f | (Seg n) holds
Sum f = (Sum g) + (f /. (len f))
let n be Nat; :: thesis: ( len f = n + 1 & g = f | (Seg n) implies Sum f = (Sum g) + (f /. (len f)) )
assume that
A1: len f = n + 1 and
A2: g = f | (Seg n) ; :: thesis: Sum f = (Sum g) + (f /. (len f))
A3: n <= len f by A1, NAT_1:11;
set q = <*(f /. (len f))*>;
set p = g ^ <*(f /. (len f))*>;
A4: len <*(f /. (len f))*> = 1 by FINSEQ_1:39;
A5: dom f = Seg (n + 1) by A1, FINSEQ_1:def 3;

A6: now :: thesis: for u being object st u in dom f holds
f . u = (g ^ <*(f /. (len f))*>) . u

let u be object ; :: thesis: ( u in dom f implies f . u = (g ^ <*(f /. (len f))*>) . u )
assume A7: u in dom f ; :: thesis: f . u = (g ^ <*(f /. (len f))*>) . u
then u in { k where k is Nat : ( 1 <= k & k <= n + 1 ) } by A5, FINSEQ_1:def 1;
then consider i being Nat such that
A8: u = i and
A9: 1 <= i and
A10: i <= n + 1 ;

now :: thesis: ( ( i = n + 1 & (g ^ <*(f /. (len f))*>) . i = f . i ) or ( i <> n + 1 & (g ^ <*(f /. (len f))*>) . i = f . i ) )

per cases ( i = n + 1 or i <> n + 1 ) ;

case A11: i = n + 1 ; :: thesis: (g ^ <*(f /. (len f))*>) . i = f . i

then ( (len g) + 1 <= i & i <= (len g) + (len <*(f /. (len f))*>) ) by A2, A3, A4, FINSEQ_1:17;
hence (g ^ <*(f /. (len f))*>) . i = <*(f /. (len f))*> . (i - (len g)) by FINSEQ_1:23
.= <*(f /. (len f))*> . ((n + 1) - n) by A2, A3, A11, FINSEQ_1:17
.= <*(f /. (len f))*> . 1 by XCMPLX_1:26
.= f /. (n + 1) by A1
.= f . i by A7, A8, A11, PARTFUN1:def 6 ;
:: thesis: verum

end;

case i <> n + 1 ; :: thesis: (g ^ <*(f /. (len f))*>) . i = f . i

then i < n + 1 by A10, XXREAL_0:1;
then i <= n by NAT_1:13;
then i in { k where k is Nat : ( 1 <= k & k <= n ) } by A9;
then i in Seg n by FINSEQ_1:def 1;
then A12: i in dom g by A2, A3, FINSEQ_1:17;
then (g ^ <*(f /. (len f))*>) . i = g . i by FINSEQ_1:def 7;
hence (g ^ <*(f /. (len f))*>) . i = f . i by A2, A12, FUNCT_1:47; :: thesis: verum

end;

end;

end;

hence f . u = (g ^ <*(f /. (len f))*>) . u by A8; :: thesis: verum

end;

len (g ^ <*(f /. (len f))*>) = (len g) + (len <*(f /. (len f))*>) by FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:40
.= len f by A1, A2, A3, FINSEQ_1:17 ;
then dom f = Seg (len (g ^ <*(f /. (len f))*>)) by FINSEQ_1:def 3
.= dom (g ^ <*(f /. (len f))*>) by FINSEQ_1:def 3 ;
then f = g ^ <*(f /. (len f))*> by A6, FUNCT_1:2;
hence Sum f = (Sum g) + (Sum <*(f /. (len f))*>) by RLVECT_1:41
.= (Sum g) + (f /. (len f)) by RLVECT_1:44 ;
:: thesis: verum