:: deftheorem Def4 defines addquaternion QUATERN2:def 4 :
for b₁ being BinOp of QUATERNION holds
( b₁ = addquaternion iff for c1, c2 being Element of QUATERNION holds b₁ . (c1,c2) = c1 + c2 );