theorem LM001: :: NDIFF_7:2

for S, T being RealNormSpace
for L being LinearOperator of S,T
for x, y being Point of S holds (L . x) - (L . y) = L . (x - y)