let z1, z2 be Quaternion; :: thesis: z1 - z2 = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) - (Im2 z2)) * <j>)) + (((Im3 z1) - (Im3 z2)) * <k>)
z1 - z2 = ((((Rea z1) + (Rea (- z2))) + (((Im1 z1) + (Im1 (- z2))) * <i>)) + (((Im2 z1) + (Im2 (- z2))) * <j>)) + (((Im3 z1) + (Im3 (- z2))) * <k>) by Lm20
.= ((((Rea z1) + (- (Rea z2))) + (((Im1 z1) + (Im1 (- z2))) * <i>)) + (((Im2 z1) + (Im2 (- z2))) * <j>)) + (((Im3 z1) + (Im3 (- z2))) * <k>) by Th34
.= ((((Rea z1) + (- (Rea z2))) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) + (Im2 (- z2))) * <j>)) + (((Im3 z1) + (Im3 (- z2))) * <k>) by Th34
.= ((((Rea z1) + (- (Rea z2))) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) + (- (Im2 z2))) * <j>)) + (((Im3 z1) + (Im3 (- z2))) * <k>) by Th34
.= ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) - (Im2 z2)) * <j>)) + (((Im3 z1) - (Im3 z2)) * <k>) by Th34 ;
hence z1 - z2 = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) - (Im2 z2)) * <j>)) + (((Im3 z1) - (Im3 z2)) * <k>) ; :: thesis: verum