let R, S be Ring; :: 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 A1: f is RingHomomorphism ; :: thesis: f . (0. R) = 0. S
f . (0. R) = f . ((0. R) + (0. R)) by RLVECT_1:4
.= (f . (0. R)) + (f . (0. R)) by A1, VECTSP_1:def 20 ;
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