theorem Th9: :: PDIFF_7:9

for m being non zero Nat
for x, y being Element of REAL
for i being Nat st 1 <= i & i <= m holds
Replace ((0* m),i,(x + y)) = (Replace ((0* m),i,x)) + (Replace ((0* m),i,y))