let z1, z2 be quaternion number ; :: thesis: ( Rea (z1 - z2) = (Rea z1) - (Rea z2) & Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) & Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) & Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) )
A1: ( z1 = [*(Rea z1),(Im1 z1),(Im2 z1),(Im3 z1)*] & z2 = [*(Rea z2),(Im1 z2),(Im2 z2),(Im3 z2)*] & z1 - z2 = [*(Rea (z1 - z2)),(Im1 (z1 - z2)),(Im2 (z1 - z2)),(Im3 (z1 - z2))*] ) by Th24;
set z2' = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*];
z2 + [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] = [*((Rea z2) + (- (Rea z2))),((Im1 z2) + (- (Im1 z2))),((Im2 z2) + (- (Im2 z2))),((Im3 z2) + (- (Im3 z2)))*] by A1, Def7
.= 0 by Lm5 ;
then - z2 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Def8;
then z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*] by A1, Def7;
hence ( Rea (z1 - z2) = (Rea z1) - (Rea z2) & Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) & Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) & Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) ) by Th23; :: thesis: verum