let R, R1 be commutative Ring; :: thesis: for f being Function of R,R1
for u being Unit of R
for v being Element of R st f is RingHomomorphism holds
f . (v * (u ["])) = (f . v) * ((f . u) ["])
let f be Function of R,R1; :: thesis: for u being Unit of R
for v being Element of R st f is RingHomomorphism holds
f . (v * (u ["])) = (f . v) * ((f . u) ["])
let u be Unit of R; :: thesis: for v being Element of R st f is RingHomomorphism holds
f . (v * (u ["])) = (f . v) * ((f . u) ["])
let v be Element of R; :: thesis: ( f is RingHomomorphism implies f . (v * (u ["])) = (f . v) * ((f . u) ["]) )
assume A1: f is RingHomomorphism ; :: thesis: f . (v * (u ["])) = (f . v) * ((f . u) ["])
then f is multiplicative ;
then f . (v * (u ["])) = (f . v) * (f . (u ["]))
.= (f . v) * ((f . u) ["]) by A1, Th12 ;
hence f . (v * (u ["])) = (f . v) * ((f . u) ["]) ; :: thesis: verum