let V, W be Z_Module; :: 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. INT.Ring)) * y) = (- (1. INT.Ring)) * (T . y) by MOD_2:def 2;
( T . (x - y) = (T . x) + (T . (- y)) & - y = (- (1. INT.Ring)) * y ) by ZMODUL01:2, VECTSP_1:def 20;
hence (T . x) - (T . y) = T . (x - y) by A1, ZMODUL01:2; :: thesis: verum