theorem Th11: :: PDIFF_7:11

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