let z1, z2 be Quaternion; :: thesis: (z1 - z2) *' = (z1 *') - (z2 *')
A1: z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*] by Th36;
A2: (- z2) *' = [*(Rea (- z2)),(- (Im1 (- z2))),(- (Im2 (- z2))),(- (Im3 (- z2)))*] by Th36;
A3: (z1 - z2) *' = [*(Rea (z1 - z2)),(- (Im1 (z1 - z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*] by Th36;
A4: (z1 *') - (z2 *') = (z1 *') + ((- z2) *') by Th48
.= [*((Rea z1) + (Rea (- z2))),((- (Im1 z1)) + (- (Im1 (- z2)))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by A1, A2, Def6
.= [*((Rea z1) + (- (Rea z2))),((- (Im1 z1)) + (- (Im1 (- z2)))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by Th34
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) - (- (Im1 z2))),((- (Im2 z1)) + (- (Im2 (- z2)))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by Th34
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) - (- (Im2 z2))),((- (Im3 z1)) + (- (Im3 (- z2))))*] by Th34
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),((- (Im3 z1)) - (- (Im3 z2)))*] by Th34
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),((- (Im3 z1)) + (Im3 z2))*] ;
(z1 - z2) *' = [*((Rea z1) - (Rea z2)),(- (Im1 (z1 - z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*] by A3, Th35
.= [*((Rea z1) - (Rea z2)),(- ((Im1 z1) - (Im1 z2))),(- (Im2 (z1 - z2))),(- (Im3 (z1 - z2)))*] by Th35
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),(- ((Im2 z1) - (Im2 z2))),(- (Im3 (z1 - z2)))*] by Th35
.= [*((Rea z1) - (Rea z2)),((- (Im1 z1)) + (Im1 z2)),((- (Im2 z1)) + (Im2 z2)),(- ((Im3 z1) - (Im3 z2)))*] by Th35 ;
hence (z1 - z2) *' = (z1 *') - (z2 *') by A4; :: thesis: verum