:: deftheorem Def6 defines multR FIELD_3:def 7 :
for R being non almost_trivial Ring
for x being non trivial Element of R
for o being object
for a, b being Element of carr (x,o) holds
( ( a = o & b = o & the multF of R . (x,x) <> x implies multR (a,b) = the multF of R . (x,x) ) & ( a <> o & b = o & the multF of R . (a,x) <> x implies multR (a,b) = the multF of R . (a,x) ) & ( a = o & b <> o & the multF of R . (x,b) <> x implies multR (a,b) = the multF of R . (x,b) ) & ( a <> o & b <> o & the multF of R . (a,b) <> x implies multR (a,b) = the multF of R . (a,b) ) & ( ( not a = o or not b = o or not the multF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the multF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the multF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the multF of R . (a,b) <> x ) implies multR (a,b) = o ) );