:: deftheorem Def4 defines addR FIELD_3:def 5 :
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 addF of R . (x,x) <> x implies addR (a,b) = the addF of R . (x,x) ) & ( a <> o & b = o & the addF of R . (a,x) <> x implies addR (a,b) = the addF of R . (a,x) ) & ( a = o & b <> o & the addF of R . (x,b) <> x implies addR (a,b) = the addF of R . (x,b) ) & ( a <> o & b <> o & the addF of R . (a,b) <> x implies addR (a,b) = the addF of R . (a,b) ) & ( ( not a = o or not b = o or not the addF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the addF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the addF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the addF of R . (a,b) <> x ) implies addR (a,b) = o ) );