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

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len (Replace ((0* m),i,(x + y))) implies (Replace ((0* m),i,(x + y))) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j )
assume A4: ( 1 <= j & j <= len (Replace ((0* m),i,(x + y))) ) ; :: thesis: (Replace ((0* m),i,(x + y))) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j
reconsider j = j as Element of NAT by ORDINAL1:def 12;
A5: dom ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) = (dom (Replace ((0* m),i,x))) /\ (dom (Replace ((0* m),i,y))) by VALUED_1:def 1;
( j in dom (Replace ((0* m),i,x)) & j in dom (Replace ((0* m),i,y)) ) by A4, A2, FINSEQ_3:25;
then j in dom ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) by A5, XBOOLE_0:def 4;
then A6: ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j = ((Replace ((0* m),i,x)) . j) + ((Replace ((0* m),i,y)) . j) by VALUED_1:def 1;

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

suppose A7: i = j ; :: thesis: (Replace ((0* m),i,(x + y))) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j

then ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j = x + ((Replace ((0* m),i,y)) . j) by A1, A6, Lm7
.= x + y by A1, A7, Lm7 ;
hence (Replace ((0* m),i,(x + y))) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j by A1, A7, Lm7; :: thesis: verum

end;

suppose A8: i <> j ; :: thesis: (Replace ((0* m),i,(x + y))) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j

then ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j = 0 + ((Replace ((0* m),i,y)) . j) by A4, A6, A2, Lm7
.= 0 by A4, A2, A8, Lm7 ;
hence (Replace ((0* m),i,(x + y))) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j by A4, A2, A8, Lm7; :: thesis: verum

end;

end;

end;

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