theorem :: QUATERNI:95

for z1, z2 being Quaternion holds z1 - z2 = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) - (Im2 z2)) * <j>)) + (((Im3 z1) - (Im3 z2)) * <k>) by Lm25;