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

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