let z be Quaternion; :: 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 Th78
.= [*(((((- (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 Th78; :: thesis: verum