:: deftheorem defmultf defines multemb FIELD_2:def 5 :
for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of carr f holds
( ( a in [#] K & b in [#] K implies multemb (f,a,b) = the multF of K . (a,b) ) & ( ( a = 0. K or b = 0. K ) implies multemb (f,a,b) = 0. K ) & ( a in [#] K & a <> 0. K & not b in [#] K implies multemb (f,a,b) = the multF of T . ((f . a),b) ) & ( b in [#] K & b <> 0. K & not a in [#] K implies multemb (f,a,b) = the multF of T . (a,(f . b)) ) & ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies multemb (f,a,b) = (f ") . ( the multF of T . (a,b)) ) & ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or multemb (f,a,b) = the multF of T . (a,b) ) );