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

proof

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

end;

A3: 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 A4: S₁[i] ; :: thesis: S₁[i + 1]

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

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

proof

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

end;

then A13: Sum (yseq | i) = r * (Sum (xseq | i)) by A7, A8, A4;
consider v being Element of REAL m such that
A14: ( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A5, A7, PDIFF_6:15;
consider w being Element of REAL m such that
A15: ( w = yseq . (len yseq) & Sum yseq = (Sum (yseq | i)) + w ) by A5, A7, A8, PDIFF_6:15;
A16: dom xseq = Seg (i + 1) by A5, FINSEQ_1:def 3;
then A17: len yseq in dom xseq by A5, FINSEQ_1:4;
then w = yseq /. (len yseq) by A15, A6, PARTFUN1:def 6
.= r * (xseq /. (len yseq)) by A5, A16, FINSEQ_1:4
.= r * v by A17, A5, A14, PARTFUN1:def 6 ;
hence Sum yseq = r * (Sum xseq) by A15, A13, A14, RVSUM_1:51; :: thesis: verum

end;

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

end;

A18: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
let xseq, yseq be FinSequence of REAL m; :: thesis: ( yseq = r (#) xseq implies Sum yseq = r * (Sum xseq) )
A19: r (#) xseq = xseq [#] r by INTEGR15:def 11;
assume A20: yseq = r (#) xseq ; :: thesis: Sum yseq = r * (Sum xseq)
then A21: dom yseq = dom xseq by A19, VALUED_2:def 39;
then A22: len xseq = len yseq by FINSEQ_3:29;
for i being Nat st i in dom xseq holds
yseq /. i = r * (xseq /. i) by A20, A21, INTEGR15:23;
hence Sum yseq = r * (Sum xseq) by A22, A18; :: thesis: verum