let z be Quaternion; :: thesis: - z = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]
A1: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by Th17;
set z9 = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*];
z + [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] = [*((Rea z) + (- (Rea z))),((Im1 z) + (- (Im1 z))),((Im2 z) + (- (Im2 z))),((Im3 z) + (- (Im3 z)))*] by A1, Def6
.= 0 by Lm6 ;
hence - z = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Def7; :: thesis: verum