theorem Th1: :: QUATERN3:1

for z1, z2 being Quaternion holds Rea (z1 * z2) = Rea (z2 * z1)