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