let F be Field; :: thesis: for W, V 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 W, V 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 . (x - y) = (T . x) + (T . (- y)) by MOD_2:def 5;
A2: - y = (- (1. F)) * y by VECTSP_1:59;
T . ((- (1. F)) * y) = (- (1. F)) * (T . y) by MOD_2:def 5;
hence (T . x) - (T . y) = T . (x - y) by A1, A2, VECTSP_1:59; :: thesis: verum