A1: 1q =
[*jj,(In (0,REAL))*]
by ARYTM_0:def 5
.=
[*jj,0,0,0*]
by QUATERNI:91
;
then A2:
( Rea 1q = 1 & Im1 1q = 0 )
by QUATERNI:23;
A3:
( Im2 1q = 0 & Im3 1q = 0 )
by A1, QUATERNI:23;
1q ^2 =
[*(((((Rea 1q) ^2) - ((Im1 1q) ^2)) - ((Im2 1q) ^2)) - ((Im3 1q) ^2)),(2 * ((Rea 1q) * (Im1 1q))),(2 * ((Rea 1q) * (Im2 1q))),(2 * ((Rea 1q) * (Im3 1q)))*]
by Th78
.=
[*jj,(In (0,REAL))*]
by A2, A3, QUATERNI:91
.=
1
by ARYTM_0:def 5
;
hence
1q ^3 = 1
; verum