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