theorem hom4a: :: RING_2:7
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 being Element of R holds f . (- x) = - (f . x)