let z be Quaternion; :: thesis: ( z = 0 implies ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 )
assume A1: z = 0 ; :: thesis: ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0
then A2: Rea z = 0 by Lm6, Th16;
A3: Im1 z = 0 by A1, Lm6, Th16;
Im2 z = 0 by A1, Lm6, Th16;
hence ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 by A1, A2, A3, Lm6, Th16; :: thesis: verum