theorem Th3: :: FIELD_2:3

for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S holds
( (f ") . (1. S) = 1. R & (f ") . (0. S) = 0. R )