let z1, z2 be quaternion number ; :: thesis: z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*]
A1: ( z1 = [*(Rea z1),(Im1 z1),(Im2 z1),(Im3 z1)*] & z2 = [*(Rea z2),(Im1 z2),(Im2 z2),(Im3 z2)*] ) by Th24;
- z2 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Th62;
hence z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*] by A1, Def7; :: thesis: verum