let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being additive Function of R,S
for x, y being Element of R holds f . (x - y) = (f . x) - (f . y)
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being additive Function of R,S
for x, y being Element of R holds f . (x - y) = (f . x) - (f . y)
let f be additive Function of R,S; :: thesis: for x, y being Element of R holds f . (x - y) = (f . x) - (f . y)
let x, y be Element of R; :: 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 hom4a ; :: thesis: verum