:: deftheorem Def10 defines R_Quaternion QUATERN2:def 10 :
for b₁ being strict doubleLoopStr holds
( b₁ = R_Quaternion iff ( the carrier of b₁ = QUATERNION & the addF of b₁ = addquaternion & the multF of b₁ = multquaternion & 1. b₁ = 1q & 0. b₁ = 0q ) );