let z be quaternion number ; :: thesis: z ^3 = - ((- z) ^3 )
A1: z ^3 = z * (z ^2 ) by QUATERN2:16;
(- z) ^3 = (- z) * ((- z) ^2 ) by QUATERN2:16
.= (- z) * (z ^2 ) by th1
.= ((- 1q ) * z) * (z ^2 ) by QUATERN2:19
.= (- 1q ) * (z * (z ^2 )) by QUATERN2:16
.= - (z ^3 ) by A1, QUATERN2:19 ;
hence z ^3 = - ((- z) ^3 ) ; :: thesis: verum