theorem :: RINGFRAC:10

for R, R1 being commutative Ring
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) ["])