let c be Quaternion; :: 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 2;
then A3: Rea c = 0 by A1, Lm3;
A4: Im1 c = 0 by A1, A2, Lm3;
A5: Im2 c = 0 by A1, A2, Lm3;
Im3 c = 0 by A1, A2, Lm3;
then c = [*0,0,0,0*] by A3, A4, A5, QUATERNI:24
.= [*(In (0,REAL)),(In (0,REAL))*] by QUATERNI:91
.= 0 by ARYTM_0:def 5 ;
hence c = 0 ; :: thesis: verum