let z1, z2 be Quaternion; :: thesis: z1 = (z1 - z2) + z2
A1: z1 = [*(Rea z1),(Im1 z1),(Im2 z1),(Im3 z1)*] by Th17;
A2: z2 = [*(Rea z2),(Im1 z2),(Im2 z2),(Im3 z2)*] by Th17;
- z2 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Th55;
then z1 - z2 = [*((Rea z1) + (- (Rea z2))),((Im1 z1) + (- (Im1 z2))),((Im2 z1) + (- (Im2 z2))),((Im3 z1) + (- (Im3 z2)))*] by A1, Def6;
then (z1 - z2) + z2 = [*(((Rea z1) + (- (Rea z2))) + (Rea z2)),(((Im1 z1) + (- (Im1 z2))) + (Im1 z2)),(((Im2 z1) + (- (Im2 z2))) + (Im2 z2)),(((Im3 z1) + (- (Im3 z2))) + (Im3 z2))*] by A2, Def6
.= [*(((Rea z1) + (Rea z2)) - (Rea z2)),(((Im1 z1) + (Im1 z2)) - (Im1 z2)),(((Im2 z1) + (Im2 z2)) - (Im2 z2)),(((Im3 z1) + (Im3 z2)) - (Im3 z2))*] ;
hence z1 = (z1 - z2) + z2 by Th17; :: thesis: verum