theorem hom4: :: RING_2:8

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
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)