:: deftheorem defines carr FIELD_2:def 2 :
for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S holds carr f = (([#] S) \ (rng f)) \/ ([#] R);