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 7
.= (f . x) * ((f . y) " ) by A1, A2, Th55 ; :: thesis: verum