let z be quaternion number ; :: thesis: z ^2 = [*(((((Rea z) ^2 ) - ((Im1 z) ^2 )) - ((Im2 z) ^2 )) - ((Im3 z) ^2 )),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*]
z ^2 = [*(Rea (z ^2 )),(Im1 (z ^2 )),(Im2 (z ^2 )),(Im3 (z ^2 ))*] by QUATERNI:24
.= [*(((((Rea z) ^2 ) - ((Im1 z) ^2 )) - ((Im2 z) ^2 )) - ((Im3 z) ^2 )),(Im1 (z ^2 )),(Im2 (z ^2 )),(Im3 (z ^2 ))*] by QUATERNI:40
.= [*(((((Rea z) ^2 ) - ((Im1 z) ^2 )) - ((Im2 z) ^2 )) - ((Im3 z) ^2 )),(2 * ((Rea z) * (Im1 z))),(Im2 (z ^2 )),(Im3 (z ^2 ))*] by QUATERNI:40
.= [*(((((Rea z) ^2 ) - ((Im1 z) ^2 )) - ((Im2 z) ^2 )) - ((Im3 z) ^2 )),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(Im3 (z ^2 ))*] by QUATERNI:40
.= [*(((((Rea z) ^2 ) - ((Im1 z) ^2 )) - ((Im2 z) ^2 )) - ((Im3 z) ^2 )),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] by QUATERNI:40 ;
hence z ^2 = [*(((((Rea z) ^2 ) - ((Im1 z) ^2 )) - ((Im2 z) ^2 )) - ((Im3 z) ^2 )),(2 * ((Rea z) * (Im1 z))),(2 * ((Rea z) * (Im2 z))),(2 * ((Rea z) * (Im3 z)))*] ; :: thesis: verum