let F be Ring; :: thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W
for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
let T be linear-transformation of V,W; :: thesis: for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
let x, y be Element of V; :: thesis: (T . x) - (T . y) = T . (x - y)
A1: T . ((- (1. F)) * y) = (- (1. F)) * (T . y) by MOD_2:def 2;
( T . (x - y) = (T . x) + (T . (- y)) & - y = (- (1. F)) * y ) by VECTSP_1:14, VECTSP_1:def 20;
hence (T . x) - (T . y) = T . (x - y) by A1, VECTSP_1:14; :: thesis: verum