z1 - z2 = ((((Rea z1) + (Rea (- z2))) + (((Im1 z1) + (Im1 (- z2))) * <i> )) + (((Im2 z1) + (Im2 (- z2))) * <j> )) + (((Im3 z1) + (Im3 (- z2))) * <k> ) by Def22
.= ((((Rea z1) + (- (Rea z2))) + (((Im1 z1) + (Im1 (- z2))) * <i> )) + (((Im2 z1) + (Im2 (- z2))) * <j> )) + (((Im3 z1) + (Im3 (- z2))) * <k> ) by Th41
.= ((((Rea z1) + (- (Rea z2))) + (((Im1 z1) - (Im1 z2)) * <i> )) + (((Im2 z1) + (Im2 (- z2))) * <j> )) + (((Im3 z1) + (Im3 (- z2))) * <k> ) by Th41
.= ((((Rea z1) + (- (Rea z2))) + (((Im1 z1) - (Im1 z2)) * <i> )) + (((Im2 z1) + (- (Im2 z2))) * <j> )) + (((Im3 z1) + (Im3 (- z2))) * <k> ) by Th41
.= ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i> )) + (((Im2 z1) - (Im2 z2)) * <j> )) + (((Im3 z1) - (Im3 z2)) * <k> ) by Th41 ;
hence for b₁ being Element of QUATERNION holds
( b₁ = z1 - z2 iff b₁ = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i> )) + (((Im2 z1) - (Im2 z2)) * <j> )) + (((Im3 z1) - (Im3 z2)) * <k> ) ) ; :: thesis: verum