let m be non zero Nat; :: thesis: for v, w, u being FinSequence of REAL m st dom v = dom w & u = v + w holds
Sum u = (Sum v) + (Sum w)
defpred S₁[ Nat] means for xseq, yseq, zseq being FinSequence of REAL m st $1 = len zseq & len zseq = len xseq & len zseq = len yseq & ( for i being Nat st i in dom zseq holds
zseq /. i = (xseq /. i) + (yseq /. i) ) holds
Sum zseq = (Sum xseq) + (Sum yseq);
A1: S₁[ 0 ]

proof

let xseq, yseq, zseq be FinSequence of REAL m; :: thesis: ( 0 = len zseq & len zseq = len xseq & len zseq = len yseq & ( for i being Nat st i in dom zseq holds
zseq /. i = (xseq /. i) + (yseq /. i) ) implies Sum zseq = (Sum xseq) + (Sum yseq) )
assume A2: ( 0 = len zseq & len zseq = len xseq & len zseq = len yseq & ( for i being Nat st i in dom zseq holds
zseq /. i = (xseq /. i) + (yseq /. i) ) ) ; :: thesis: Sum zseq = (Sum xseq) + (Sum yseq)
then A3: ( Sum zseq = 0* m & Sum yseq = 0* m ) by EUCLID_7:def 11;
0* m = 0. (TOP-REAL m) by EUCLID:70;
then (Sum xseq) + (Sum yseq) = (0. (TOP-REAL m)) + (0. (TOP-REAL m)) by A2, A3, EUCLID_7:def 11
.= 0. (TOP-REAL m) by RLVECT_1:4 ;
hence Sum zseq = (Sum xseq) + (Sum yseq) by A3, EUCLID:70; :: thesis: verum

end;

A4: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]

now :: thesis: for xseq, yseq, zseq being FinSequence of REAL m st i + 1 = len zseq & len zseq = len xseq & len zseq = len yseq & ( for k being Nat st k in dom zseq holds
zseq /. k = (xseq /. k) + (yseq /. k) ) holds
Sum zseq = (Sum xseq) + (Sum yseq)

let xseq, yseq, zseq be FinSequence of REAL m; :: thesis: ( i + 1 = len zseq & len zseq = len xseq & len zseq = len yseq & ( for k being Nat st k in dom zseq holds
zseq /. k = (xseq /. k) + (yseq /. k) ) implies Sum zseq = (Sum xseq) + (Sum yseq) )
assume A6: ( i + 1 = len zseq & len zseq = len xseq & len zseq = len yseq & ( for k being Nat st k in dom zseq holds
zseq /. k = (xseq /. k) + (yseq /. k) ) ) ; :: thesis: Sum zseq = (Sum xseq) + (Sum yseq)
set xseq0 = xseq | i;
set yseq0 = yseq | i;
set zseq0 = zseq | i;
A7: ( dom xseq = dom yseq & dom zseq = dom yseq ) by A6, FINSEQ_3:29;
A8: i = len (xseq | i) by A6, FINSEQ_1:59, NAT_1:11;
then A9: ( len (xseq | i) = len (yseq | i) & len (xseq | i) = len (zseq | i) ) by A6, FINSEQ_1:59, NAT_1:11;
for k being Nat st k in dom (zseq | i) holds
(zseq | i) /. k = ((xseq | i) /. k) + ((yseq | i) /. k)

proof

let k be Nat; :: thesis: ( k in dom (zseq | i) implies (zseq | i) /. k = ((xseq | i) /. k) + ((yseq | i) /. k) )
assume A10: k in dom (zseq | i) ; :: thesis: (zseq | i) /. k = ((xseq | i) /. k) + ((yseq | i) /. k)
then A11: ( k in dom (yseq | (Seg i)) & k in dom (xseq | (Seg i)) & k in dom (zseq | (Seg i)) ) by A9, FINSEQ_3:29;
A12: ( k in Seg i & k in dom zseq ) by A10, RELAT_1:57;
then A13: zseq /. k = (xseq /. k) + (yseq /. k) by A6;
A14: xseq /. k = xseq . k by A12, A7, PARTFUN1:def 6
.= (xseq | (Seg i)) . k by A12, FUNCT_1:49
.= (xseq | (Seg i)) /. k by A11, PARTFUN1:def 6 ;
A15: yseq /. k = yseq . k by A7, A12, PARTFUN1:def 6
.= (yseq | (Seg i)) . k by A12, FUNCT_1:49
.= (yseq | (Seg i)) /. k by A11, PARTFUN1:def 6 ;
(zseq | i) /. k = (zseq | (Seg i)) . k by A10, PARTFUN1:def 6
.= zseq . k by A12, FUNCT_1:49 ;
hence (zseq | i) /. k = ((xseq | i) /. k) + ((yseq | i) /. k) by A13, A14, A15, A12, PARTFUN1:def 6; :: thesis: verum

end;

then A16: Sum (zseq | i) = (Sum (xseq | i)) + (Sum (yseq | i)) by A8, A9, A5;
consider v being Element of REAL m such that
A17: ( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A6, A8, PDIFF_6:15;
consider w being Element of REAL m such that
A18: ( w = yseq . (len yseq) & Sum yseq = (Sum (yseq | i)) + w ) by A6, A8, A9, PDIFF_6:15;
consider t being Element of REAL m such that
A19: ( t = zseq . (len zseq) & Sum zseq = (Sum (zseq | i)) + t ) by A6, A8, A9, PDIFF_6:15;
A20: dom zseq = Seg (i + 1) by A6, FINSEQ_1:def 3;
then len zseq in dom zseq by A6, FINSEQ_1:4;
then t = zseq /. (len zseq) by A19, PARTFUN1:def 6;
then A21: t = (xseq /. (len xseq)) + (yseq /. (len yseq)) by A6, A20, FINSEQ_1:4;
( dom xseq = Seg (i + 1) & dom yseq = Seg (i + 1) ) by A6, FINSEQ_1:def 3;
then A22: ( v = xseq /. (len xseq) & w = yseq /. (len yseq) ) by A6, A17, A18, FINSEQ_1:4, PARTFUN1:def 6;
reconsider F1 = Sum (xseq | i) as real-valued FinSequence ;
reconsider F2 = Sum (yseq | i) as real-valued FinSequence ;
reconsider F3 = xseq /. (len xseq) as real-valued FinSequence ;
reconsider F4 = yseq /. (len yseq) as real-valued FinSequence ;
Sum zseq = ((F1 + F2) + F3) + F4 by A19, A16, A21, RVSUM_1:15;
then Sum zseq = ((F1 + F3) + F2) + F4 by RVSUM_1:15;
hence Sum zseq = (Sum xseq) + (Sum yseq) by A22, A17, A18, RVSUM_1:15; :: thesis: verum

end;

hence S₁[i + 1] ; :: thesis: verum

end;

A23: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A4);
let xseq, yseq, zseq be FinSequence of REAL m; :: thesis: ( dom xseq = dom yseq & zseq = xseq + yseq implies Sum zseq = (Sum xseq) + (Sum yseq) )
assume A24: ( dom xseq = dom yseq & zseq = xseq + yseq ) ; :: thesis: Sum zseq = (Sum xseq) + (Sum yseq)
then A25: len yseq = len xseq by FINSEQ_3:29;
xseq + yseq = xseq <++> yseq by INTEGR15:def 9;
then dom zseq = (dom xseq) /\ (dom yseq) by A24, VALUED_2:def 45;
then A26: len zseq = len xseq by A24, FINSEQ_3:29;
for i being Nat st i in dom zseq holds
zseq /. i = (xseq /. i) + (yseq /. i) by A24, INTEGR15:21;
hence Sum zseq = (Sum xseq) + (Sum yseq) by A25, A26, A23; :: thesis: verum