let f, g be FinSequence of COMPLEX ; :: thesis: for n being Nat st len f = n + 1 & g = f | n holds
Sum f = (Sum g) + (f /. (len f))
let n be Nat; :: thesis: ( len f = n + 1 & g = f | n implies Sum f = (Sum g) + (f /. (len f)) )
assume that
A1: len f = n + 1 and
A2: g = f | n ; :: thesis: Sum f = (Sum g) + (f /. (len f))
A3: dom f = Seg (n + 1) by A1, FINSEQ_1:def 3;
set q = <*(f /. (len f))*>;
set p = g ^ <*(f /. (len f))*>;
A4: len <*(f /. (len f))*> = 1 by FINSEQ_1:39;
set n9 = Seg n;
A5: g = f | (Seg n) by A2, FINSEQ_1:def 16;
A6: n <= len f by A1, NAT_1:11;

A7: 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 A8: 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 A3, FINSEQ_1:def 1;
then consider i being Nat such that
A9: u = i and
A10: 1 <= i and
A11: 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 A12: i = n + 1 ; :: thesis: (g ^ <*(f /. (len f))*>) . i = f . i

then A13: (len g) + 1 <= i by A1, A2, FINSEQ_1:59, NAT_1:11;
i <= (len g) + (len <*(f /. (len f))*>) by A1, A2, A4, A12, FINSEQ_1:59, NAT_1:11;
hence (g ^ <*(f /. (len f))*>) . i = <*(f /. (len f))*> . (i - (len g)) by A13, FINSEQ_1:23
.= <*(f /. (len f))*> . ((n + 1) - n) by A1, A2, A12, FINSEQ_1:59, NAT_1:11
.= f /. (n + 1) by A1, FINSEQ_1:40
.= f . i by A8, A9, A12, PARTFUN1:def 6 ;
:: thesis: verum

end;

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

then i < n + 1 by A11, XXREAL_0:1;
then i <= n by NAT_1:13;
then i in { k where k is Nat : ( 1 <= k & k <= n ) } by A10;
then i in Seg n by FINSEQ_1:def 1;
then A14: i in dom g by A5, A6, 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 A5, A14, FUNCT_1:47; :: thesis: verum

end;

end;

end;

hence f . u = (g ^ <*(f /. (len f))*>) . u by A9; :: 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, FINSEQ_1:59, NAT_1:11 ;
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 A7, FUNCT_1:2;
hence Sum f = (Sum g) + (Sum <*(f /. (len f))*>) by Th44
.= (Sum g) + (f /. (len f)) by FINSOP_1:11 ;
:: thesis: verum