:: deftheorem defines ^3 QUATERN3:def 2 :
for z being Quaternion holds z ^3 = (z * z) * z;