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

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