let R, S be non degenerated almost_left_invertible commutative Ring; :: thesis: for f being Function of R,S st f is RingHomomorphism holds
for x, y being Element of R st y <> 0. R holds
f . (x * (y ")) = (f . x) * ((f . y) ")
let f be Function of R,S; :: thesis: ( f is RingHomomorphism implies for x, y being Element of R st y <> 0. R holds
f . (x * (y ")) = (f . x) * ((f . y) ") )
assume A1: f is RingHomomorphism ; :: thesis: for x, y being Element of R st y <> 0. R holds
f . (x * (y ")) = (f . x) * ((f . y) ")
let x, y be Element of R; :: thesis: ( y <> 0. R implies f . (x * (y ")) = (f . x) * ((f . y) ") )
assume A2: y <> 0. R ; :: thesis: f . (x * (y ")) = (f . x) * ((f . y) ")
thus f . (x * (y ")) = (f . x) * (f . (y ")) by A1, GROUP_6:def 6
.= (f . x) * ((f . y) ") by A1, A2, Th52 ; :: thesis: verum