let z be Quaternion; :: 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 Th81
.= ((- 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