let m be non zero Nat; :: thesis: for x, a being Real
for i being Nat st 1 <= i & i <= m holds
(0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x))
let x, a be Real; :: thesis: for i being Nat st 1 <= i & i <= m holds
(0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x))
let i be Nat; :: thesis: ( 1 <= i & i <= m implies (0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x)) )
assume A1: ( 1 <= i & i <= m ) ; :: thesis: (0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x))
reconsider ax = a * x as Real ;
A2: ( len (Replace ((0* m),i,ax)) = m & len (Replace ((0* m),i,x)) = m ) by Lm6;
then A3: len (a * (Replace ((0* m),i,x))) = len (Replace ((0* m),i,ax)) by RVSUM_1:117;
for j being Nat st 1 <= j & j <= len (Replace ((0* m),i,ax)) holds
(Replace ((0* m),i,ax)) . j = (a * (Replace ((0* m),i,x))) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len (Replace ((0* m),i,ax)) implies (Replace ((0* m),i,ax)) . j = (a * (Replace ((0* m),i,x))) . j )
assume A4: ( 1 <= j & j <= len (Replace ((0* m),i,ax)) ) ; :: thesis: (Replace ((0* m),i,ax)) . j = (a * (Replace ((0* m),i,x))) . j
reconsider j = j as Nat ;

per cases ( i = j or i <> j ) ;

suppose A5: i = j ; :: thesis: (Replace ((0* m),i,ax)) . j = (a * (Replace ((0* m),i,x))) . j

then (Replace ((0* m),i,ax)) . j = a * x by A1, Lm7
.= a * ((Replace ((0* m),i,x)) . j) by A1, A5, Lm7 ;
hence (Replace ((0* m),i,ax)) . j = (a * (Replace ((0* m),i,x))) . j by RVSUM_1:44; :: thesis: verum

end;

suppose A6: i <> j ; :: thesis: (Replace ((0* m),i,ax)) . j = (a * (Replace ((0* m),i,x))) . j

then (Replace ((0* m),i,x)) . j = 0 by A2, A4, Lm7;
then (Replace ((0* m),i,ax)) . j = a * ((Replace ((0* m),i,x)) . j) by A2, A4, A6, Lm7;
hence (Replace ((0* m),i,ax)) . j = (a * (Replace ((0* m),i,x))) . j by RVSUM_1:44; :: thesis: verum

end;

end;

end;

hence (0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x)) by A3; :: thesis: verum