let r be quaternion number ; :: thesis: ( r <> 0 implies |.r.| <> 0 )
assume A1: r <> 0 ; :: thesis: |.r.| <> 0
assume A2: |.r.| = 0 ; :: thesis: contradiction
consider r0, r1, r2, r3 being Element of REAL such that
A3: r = [*r0,r1,r2,r3*] by QUA7;
A4: ( Rea r = r0 & Im1 r = r1 & Im2 r = r2 & Im3 r = r3 ) by A3, QUATERNI:23;
A5: 0 <= ((((Rea r) ^2 ) + ((Im1 r) ^2 )) + ((Im2 r) ^2 )) + ((Im3 r) ^2 ) by QUATERNI:74;
|.r.| ^2 = (((r0 ^2 ) + (r1 ^2 )) + (r2 ^2 )) + (r3 ^2 ) by A4, A5, SQUARE_1:def 4;
then ( r0 = 0 & r1 = 0 & r2 = 0 & r3 = 0 ) by A2, Lm2;
then r = [*0 ,0 *] by A3, QUATERNI:def 6, QUATERNI:91
.= 0 by ARYTM_0:def 7 ;
hence contradiction by A1; :: thesis: verum