let z1, z2 be Quaternion; :: thesis: z1 / z2 = [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*]
z1 / z2 = [*(Rea (z1 / z2)),(Im1 (z1 / z2)),(Im2 (z1 / z2)),(Im3 (z1 / z2))*] by QUATERNI:24
.= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),(Im1 (z1 / z2)),(Im2 (z1 / z2)),(Im3 (z1 / z2))*] by QUATERN2:30
.= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),(Im2 (z1 / z2)),(Im3 (z1 / z2))*] by QUATERN2:30
.= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),(Im3 (z1 / z2))*] by QUATERN2:30
.= [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*] by QUATERN2:30 ;
hence z1 / z2 = [*((((((Rea z2) * (Rea z1)) + ((Im1 z1) * (Im1 z2))) + ((Im2 z2) * (Im2 z1))) + ((Im3 z2) * (Im3 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im1 z1)) - ((Im1 z2) * (Rea z1))) - ((Im2 z2) * (Im3 z1))) + ((Im3 z2) * (Im2 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im2 z1)) + ((Im1 z2) * (Im3 z1))) - ((Im2 z2) * (Rea z1))) - ((Im3 z2) * (Im1 z1))) / (|.z2.| ^2)),((((((Rea z2) * (Im3 z1)) - ((Im1 z2) * (Im2 z1))) + ((Im2 z2) * (Im1 z1))) - ((Im3 z2) * (Rea z1))) / (|.z2.| ^2))*] ; :: thesis: verum