let m be non empty Element of NAT ; :: thesis: for x, a being Element of REAL
for i being Element of NAT st 1 <= i & i <= m holds
Replace (0* m),i,(a * x) = a * (Replace (0* m),i,x)
let x, a be Element of REAL ; :: thesis: for i being Element of NAT st 1 <= i & i <= m holds
Replace (0* m),i,(a * x) = a * (Replace (0* m),i,x)
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= m implies Replace (0* m),i,(a * x) = a * (Replace (0* m),i,x) )
assume A1: ( 1 <= i & i <= m ) ; :: thesis: Replace (0* m),i,(a * x) = a * (Replace (0* m),i,x)
A2: ( len (Replace (0* m),i,(a * x)) = m & len (Replace (0* m),i,x) = m ) by Lm6;
then A3: len (a * (Replace (0* m),i,x)) = len (Replace (0* m),i,(a * x)) by RVSUM_1:147;
for j being Nat st 1 <= j & j <= len (Replace (0* m),i,(a * x)) holds
(Replace (0* m),i,(a * x)) . j = (a * (Replace (0* m),i,x)) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len (Replace (0* m),i,(a * x)) implies (Replace (0* m),i,(a * x)) . j = (a * (Replace (0* m),i,x)) . j )
assume A4: ( 1 <= j & j <= len (Replace (0* m),i,(a * x)) ) ; :: thesis: (Replace (0* m),i,(a * x)) . j = (a * (Replace (0* m),i,x)) . j
reconsider j = j as Element of NAT by ORDINAL1:def 13;

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

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

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

end;

suppose A6: i <> j ; :: thesis: (Replace (0* m),i,(a * x)) . 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,(a * x)) . j = a * ((Replace (0* m),i,x) . j) by A2, A4, A6, Lm7;
hence (Replace (0* m),i,(a * x)) . j = (a * (Replace (0* m),i,x)) . j by RVSUM_1:66; :: thesis: verum

end;

end;

end;

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