z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*] by Lm14;
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> ) ) by Lm20; :: thesis: verum