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 f is RingHomomorphism ; :: thesis: for x being Element of R st x <> 0. R holds
f . (x " ) = (f . x) "
then A1: ( f is multiplicative & f is unity-preserving ) ;
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 7
.= f . (1_ R) by A2, VECTSP_1:def 22
.= 1_ S by A1, GROUP_1:def 17 ;
then f . x <> 0. S by VECTSP_1:39;
hence f . (x " ) = (f . x) " by A3, VECTSP_1:def 22; :: thesis: verum