let z1, z2, z3 be Quaternion; :: thesis: Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2)
Rea ((z1 * z2) * z3) = Rea (z1 * (z2 * z3)) by QUATERN2:16
.= Rea ((z2 * z3) * z1) by Th1
.= Rea (z2 * (z3 * z1)) by QUATERN2:16
.= Rea ((z3 * z1) * z2) by Th1 ;
hence Rea ((z1 * z2) * z3) = Rea ((z3 * z1) * z2) ; :: thesis: verum