let z be Quaternion; 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; verum