let c be quaternion number ; :: thesis: ( c .|. c = 0 implies c = 0 )
assume c .|. c = 0 ; :: thesis: c = 0
then A1a: |.c.| ^2 = 0 by Thd5a;
A2: ((((Rea c) ^2 ) + ((Im1 c) ^2 )) + ((Im2 c) ^2 )) + ((Im3 c) ^2 ) >= 0 by Lm4;
A3: |.c.| ^2 = ((((Rea c) ^2 ) + ((Im1 c) ^2 )) + ((Im2 c) ^2 )) + ((Im3 c) ^2 ) by A2, SQUARE_1:def 4;
( Rea c = 0 & Im1 c = 0 & Im2 c = 0 & Im3 c = 0 ) by A1a, A3, Lm5;
then c = [*0 ,0 ,0 ,0 *] by QUATERNI:24
.= [*0 ,0 *] by QUATERNI:def 6, QUATERNI:91
.= 0 by ARYTM_0:def 7 ;
hence c = 0 ; :: thesis: verum