let z1, z2 be Quaternion; 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)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*]
by Lm13;
hence
z1 + z2 = ((((Rea z1) + (Rea z2)) + (((Im1 z1) + (Im1 z2)) * <i>)) + (((Im2 z1) + (Im2 z2)) * <j>)) + (((Im3 z1) + (Im3 z2)) * <k>)
by Lm19; verum