:: deftheorem defines ^2 QUATERN3:def 1 :
for z being Quaternion holds z ^2 = z * z;