theorem Th53: :: QUOFIELD:53

for R, S being non degenerated almost_left_invertible commutative Ring
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) ")