let S, T be RealNormSpace; :: thesis: for L being LinearOperator of S,T
for x, y being Point of S holds (L . x) - (L . y) = L . (x - y)
let L be LinearOperator of S,T; :: thesis: for x, y being Point of S holds (L . x) - (L . y) = L . (x - y)
let x, x0 be Point of S; :: thesis: (L . x) - (L . x0) = L . (x - x0)
thus (L . x) - (L . x0) = (L . x) + ((- 1) * (L . x0)) by RLVECT_1:16
.= (L . x) + (L . ((- 1) * x0)) by LOPBAN_1:def 5
.= L . (x + ((- 1) * x0)) by VECTSP_1:def 20
.= L . (x - x0) by RLVECT_1:16 ; :: thesis: verum