let R be non empty Abelian add-associative right_zeroed addLoopStr ; for p, q being FinSequence of the carrier of R st dom p = dom q holds
Sum (p + q) = (Sum p) + (Sum q)
let p, q be FinSequence of the carrier of R; ( dom p = dom q implies Sum (p + q) = (Sum p) + (Sum q) )
consider fp being sequence of the carrier of R such that
A1:
Sum p = fp . (len p)
and
A2:
fp . 0 = 0. R
and
A3:
for j being Nat
for v being Element of R st j < len p & v = p . (j + 1) holds
fp . (j + 1) = (fp . j) + v
by RLVECT_1:def 12;
consider fq being sequence of the carrier of R such that
A4:
Sum q = fq . (len q)
and
A5:
fq . 0 = 0. R
and
A6:
for j being Nat
for v being Element of R st j < len q & v = q . (j + 1) holds
fq . (j + 1) = (fq . j) + v
by RLVECT_1:def 12;
assume
dom p = dom q
; Sum (p + q) = (Sum p) + (Sum q)
then A7: Seg (len p) =
dom q
by FINSEQ_1:def 3
.=
Seg (len q)
by FINSEQ_1:def 3
;
then A8:
len q = len p
by FINSEQ_1:6;
consider fa being sequence of the carrier of R such that
A9:
Sum (p + q) = fa . (len (p + q))
and
A10:
fa . 0 = 0. R
and
A11:
for j being Nat
for v being Element of R st j < len (p + q) & v = (p + q) . (j + 1) holds
fa . (j + 1) = (fa . j) + v
by RLVECT_1:def 12;
defpred S1[ Nat] means (fp . $1) + (fq . $1) = fa . $1;
A12: Seg (len p) =
dom p
by FINSEQ_1:def 3
.=
dom (p + q)
by Def1
.=
Seg (len (p + q))
by FINSEQ_1:def 3
;
then A13:
len (p + q) = len p
by FINSEQ_1:6;
A14:
now for j being Element of NAT st 0 <= j & j < len p & S1[j] holds
S1[j + 1]let j be
Element of
NAT ;
( 0 <= j & j < len p & S1[j] implies S1[j + 1] )assume that
0 <= j
and A15:
j < len p
;
( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
verumproof
assume A16:
S1[
j]
;
S1[j + 1]
A17:
0 + 1
<= j + 1
by XREAL_1:6;
A18:
j + 1
<= len p
by A15, NAT_1:13;
then
j + 1
in Seg (len p)
by A17, FINSEQ_1:1;
then
j + 1
in dom p
by FINSEQ_1:def 3;
then A19:
p /. (j + 1) = p . (j + 1)
by PARTFUN1:def 6;
j + 1
in Seg (len q)
by A7, A18, A17, FINSEQ_1:1;
then
j + 1
in dom q
by FINSEQ_1:def 3;
then A20:
q /. (j + 1) = q . (j + 1)
by PARTFUN1:def 6;
A21:
j + 1
<= len (p + q)
by A13, A15, NAT_1:13;
then
j + 1
in Seg (len (p + q))
by A17, FINSEQ_1:1;
then
j + 1
in dom (p + q)
by FINSEQ_1:def 3;
then
(p + q) /. (j + 1) = (p + q) . (j + 1)
by PARTFUN1:def 6;
then fa . (j + 1) =
(fa . j) + ((p + q) /. (j + 1))
by A13, A11, A15
.=
((fp . j) + (fq . j)) + ((p /. (j + 1)) + (q /. (j + 1)))
by A16, A21, A17, Def1
.=
(fp . j) + ((fq . j) + ((p /. (j + 1)) + (q /. (j + 1))))
by RLVECT_1:def 3
.=
(fp . j) + ((p /. (j + 1)) + ((fq . j) + (q /. (j + 1))))
by RLVECT_1:def 3
.=
((fp . j) + (p /. (j + 1))) + ((fq . j) + (q /. (j + 1)))
by RLVECT_1:def 3
.=
(fp . (j + 1)) + ((fq . j) + (q /. (j + 1)))
by A3, A15, A19
.=
(fp . (j + 1)) + (fq . (j + 1))
by A8, A6, A15, A20
;
hence
S1[
j + 1]
;
verum
end; end;
A22:
S1[ 0 ]
by A2, A5, A10, RLVECT_1:def 4;
A23:
for i being Element of NAT st 0 <= i & i <= len p holds
S1[i]
from INT_1:sch 7(A22, A14);
thus Sum (p + q) =
fa . (len p)
by A12, A9, FINSEQ_1:6
.=
(Sum p) + (Sum q)
by A8, A1, A4, A23
; verum