let z1, z2 be Quaternion; :: 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) )
z1 - z2 = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) - (Im2 z2)) * <j>)) + (((Im3 z1) - (Im3 z2)) * <k>) by Lm25;
then z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*] by Lm19;
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 Th16; :: thesis: verum