let c be quaternion number ; :: 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 QUA7;
|.c.| > 0 by A1, Th40;
then A3: |.c.| ^2 > 0 by SQUARE_1:74;
A4: ( Rea c = x1 & Im1 c = x2 & Im2 c = x3 & Im3 c = x4 ) by A2, QUATERNI:23;
A5: (((x1 ^2 ) + (x2 ^2 )) + (x3 ^2 )) + (x4 ^2 ) >= 0 by Lm4;
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, SQUARE_1:def 4
.= [*1,0 ,0 ,0 *] by A3, XCMPLX_1:60
.= [*1,0 *] by QUATERNI:def 6, QUATERNI:91
.= 1 by ARYTM_0:def 7 ;
hence c / c = 1q ; :: thesis: verum