theorem Th12: :: PDIFF_7:12

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