let c be Quaternion; :: thesis: ( c <> 0q implies c / c = 1q )
assume A1: c <> 0q ; :: thesis: c / c = 1q
consider x1, x2, x3, x4 being Element of REAL such that
A2: c = [*x1,x2,x3,x4*] by Lm1;
|.c.| > 0 by A1, Th10;
then A3: |.c.| ^2 > 0 by SQUARE_1:12;
A4: Rea c = x1 by A2, QUATERNI:23;
A5: Im1 c = x2 by A2, QUATERNI:23;
A6: Im2 c = x3 by A2, QUATERNI:23;
A7: Im3 c = x4 by A2, QUATERNI:23;
A8: (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) >= 0 by Lm2;
c / c = [*(((((x1 * x1) + (x2 * x2)) + (x3 * x3)) + (x4 * x4)) / (|.c.| ^2)),(((((x1 * x2) - (x2 * x1)) - (x3 * x4)) + (x4 * x3)) / (|.c.| ^2)),(((((x1 * x3) + (x2 * x4)) - (x3 * x1)) - (x4 * x2)) / (|.c.| ^2)),(((((x1 * x4) - (x2 * x3)) + (x3 * x2)) - (x4 * x1)) / (|.c.| ^2))*] by A2, Def1
.= [*((|.c.| ^2) / (|.c.| ^2)),0,0,0*] by A4, A5, A6, A7, A8, SQUARE_1:def 2
.= [*1,0,0,0*] by A3, XCMPLX_1:60
.= [*jj,(In (0,REAL))*] by QUATERNI:91
.= 1 by ARYTM_0:def 5 ;
hence c / c = 1q ; :: thesis: verum