let z be quaternion number ; :: thesis: z ^2 = (- z) ^2
(- 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))))*] by Th82
.= [*(((((- (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:41
.= [*(((((- (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:41
.= [*(((((- (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:41
.= [*(((((- (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:41
.= [*(((((- (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:41
.= [*(((((- (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:41
.= [*(((((- (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:41
.= [*(((((- (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:41
.= [*(((((- (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:41
.= [*(((((- (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:41
.= [*(((((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)))*] ;
hence z ^2 = (- z) ^2 by Th82; :: thesis: verum