:: deftheorem defaddf defines addemb FIELD_2:def 3 :
for R being Ring
for S being b₁ -monomorphic Ring
for f being Monomorphism of R,S
for a, b being Element of carr f holds
( ( a in [#] R & b in [#] R implies addemb (f,a,b) = the addF of R . (a,b) ) & ( a in [#] R & not b in [#] R implies addemb (f,a,b) = the addF of S . ((f . a),b) ) & ( b in [#] R & not a in [#] R implies addemb (f,a,b) = the addF of S . (a,(f . b)) ) & ( not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f implies addemb (f,a,b) = (f ") . ( the addF of S . (a,b)) ) & ( ( not a in [#] R or not b in [#] R ) & ( not a in [#] R or b in [#] R ) & ( not b in [#] R or a in [#] R ) & ( a in [#] R or b in [#] R or not the addF of S . (a,b) in rng f ) implies addemb (f,a,b) = the addF of S . (a,b) ) );