:: deftheorem defines invquaternion QUATERN2:def 8 :
for b₁ being UnOp of QUATERNION holds
( b₁ = invquaternion iff for c being Element of QUATERNION holds b₁ . c = c " );