let z be Quaternion; :: thesis: - z = (((- (Rea z)) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>)
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 Lm19;
[*(- (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 Lm13
.= [*((- (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 Th16
.= [*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 Th16
.= [*0,0,((- (Im2 z)) + (Im2 z)),((Im3 [*(- (Rea z)),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]) + (Im3 z))*] by Th16
.= [*0,0,0,((- (Im3 z)) + (Im3 z))*] by Th16
.= 0 by Lm6 ;
hence - z = (((- (Rea z)) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) by A1, Def7; :: thesis: verum