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