let R be non empty Abelian add-associative right_zeroed addLoopStr ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 S₁[ 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 :: thesis: for j being Element of NAT st 0 <= j & j < len p & S₁[j] holds
S₁[j + 1]

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len p & S₁[j] implies S₁[j + 1] )
assume that
0 <= j and
A15: j < len p ; :: thesis: ( S₁[j] implies S₁[j + 1] )
thus ( S₁[j] implies S₁[j + 1] ) :: thesis: verum

proof

assume A16: S₁[j] ; :: thesis: S₁[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 S₁[j + 1] ; :: thesis: verum

end;

end;

A22: S₁[ 0 ] by A2, A5, A10, RLVECT_1:def 4;
A23: for i being Element of NAT st 0 <= i & i <= len p holds
S₁[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 ; :: thesis: verum