theorem Th1: :: FIELD_2:1

for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for a, b being Element of rng f holds
( (f ") . (a + b) = ((f ") . a) + ((f ") . b) & (f ") . (a * b) = ((f ") . a) * ((f ") . b) )