let G, H be AddGroup; :: thesis: for f being Homomorphism of G,H

for x, y being Element of G holds f . (x - y) = (f . x) - (f . y)

let f be Homomorphism of G,H; :: thesis: for x, y being Element of G holds f . (x - y) = (f . x) - (f . y)

let x, y be Element of G; :: thesis: f . (x - y) = (f . x) - (f . y)

thus f . (x - y) = (f . x) + (f . (- y)) by VECTSP_1:def 20

.= (f . x) - (f . y) by Lm14 ; :: thesis: verum

for x, y being Element of G holds f . (x - y) = (f . x) - (f . y)

let f be Homomorphism of G,H; :: thesis: for x, y being Element of G holds f . (x - y) = (f . x) - (f . y)

let x, y be Element of G; :: thesis: f . (x - y) = (f . x) - (f . y)

thus f . (x - y) = (f . x) + (f . (- y)) by VECTSP_1:def 20

.= (f . x) - (f . y) by Lm14 ; :: thesis: verum