set z9 = [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*];
A1:
[*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] = (((- (Rea z)) + ((- (Im1 z)) * <i> )) + ((- (Im2 z)) * <j> )) + ((- (Im3 z)) * <k> )
by Lm20;
[*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] + z =
[*((Rea [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Rea z)),((Im1 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im1 z)),((Im2 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*]
by Lm14
.=
[*((- (Rea z)) + (Rea z)),((Im1 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im1 z)),((Im2 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*]
by Th23
.=
[*0 ,((- (Im1 z)) + (Im1 z)),((Im2 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*]
by Th23
.=
[*0 ,0 ,((- (Im2 z)) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*]
by Th23
.=
[*0 ,0 ,0 ,((- (Im3 z)) + (Im3 z))*]
by Th23
.=
0
by Lm7
;
hence
for b1 being Element of QUATERNION holds
( b1 = - z iff b1 = (((- (Rea z)) + ((- (Im1 z)) * <i> )) + ((- (Im2 z)) * <j> )) + ((- (Im3 z)) * <k> ) )
by A1, Def8; verum