let R, S be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for f being Function of R,S st f is RingHomomorphism holds
f . (0. R) = 0. S
let f be Function of R,S; :: thesis: ( f is RingHomomorphism implies f . (0. R) = 0. S )
assume f is RingHomomorphism ; :: thesis: f . (0. R) = 0. S
then A1: f is additive ;
f . (0. R) = f . ((0. R) + (0. R)) by RLVECT_1:4
.= (f . (0. R)) + (f . (0. R)) by A1 ;
then 0. S = ((f . (0. R)) + (f . (0. R))) + (- (f . (0. R))) by RLVECT_1:def 10
.= (f . (0. R)) + ((f . (0. R)) + (- (f . (0. R)))) by RLVECT_1:def 3
.= (f . (0. R)) + (0. S) by RLVECT_1:def 10
.= f . (0. R) by RLVECT_1:4 ;
hence f . (0. R) = 0. S ; :: thesis: verum