:: deftheorem Def9 defines G_Quaternion QUATERN2:def 9 :
for b₁ being strict addLoopStr holds
( b₁ = G_Quaternion iff ( the carrier of b₁ = QUATERNION & the addF of b₁ = addquaternion & 0. b₁ = 0q ) );