let m be non zero Nat; 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; 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; ( 1 <= i & i <= m implies (0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x)) )
assume A1:
( 1 <= i & i <= m )
; (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;
( 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)) )
;
(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
;
(Replace ((0* m),i,ax)) . j = (a * (Replace ((0* m),i,x))) . jthen (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;
verum end; suppose A6:
i <> j
;
(Replace ((0* m),i,ax)) . j = (a * (Replace ((0* m),i,x))) . jthen
(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;
verum end;
end;
hence
(0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x))
by A3; verum