let c be Quaternion; ( c .|. c = 0 implies c = 0 )
assume
c .|. c = 0
; 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
; verum