let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; 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; 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; ( 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)
; 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 for u being object st u in dom f holds
f . u = (g ^ <*(f /. (len f))*>) . ulet u be
object ;
( u in dom f implies f . u = (g ^ <*(f /. (len f))*>) . u )assume A7:
u in dom f
;
f . u = (g ^ <*(f /. (len f))*>) . uthen
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 ( ( 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
;
(g ^ <*(f /. (len f))*>) . i = f . ithen
(
(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, FINSEQ_1:40
.=
f . i
by A7, A8, A11, PARTFUN1:def 6
;
verum end; end; end; hence
f . u = (g ^ <*(f /. (len f))*>) . u
by A8;
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
;
verum