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 being Element of R st x <> 0. R holds
f . (x ") = (f . x) "
let f be Function of R,S; :: thesis: ( f is RingHomomorphism implies for x being Element of R st x <> 0. R holds
f . (x ") = (f . x) " )
assume A1: f is RingHomomorphism ; :: thesis: for x being Element of R st x <> 0. R holds
f . (x ") = (f . x) "
let x be Element of R; :: thesis: ( x <> 0. R implies f . (x ") = (f . x) " )
assume A2: x <> 0. R ; :: thesis: f . (x ") = (f . x) "
A3: (f . x) * (f . (x ")) = f . ((x ") * x) by A1, GROUP_6:def 6
.= f . (1_ R) by A2, VECTSP_1:def 10
.= 1_ S by A1, GROUP_1:def 13 ;
then f . x <> 0. S ;
hence f . (x ") = (f . x) " by A3, VECTSP_1:def 10; :: thesis: verum