let a, b be Real; :: thesis: ( |.(a + b).| = |.a.| + |.b.| iff |.(a - b).| = |.(|.a.| - |.b.|).| )
reconsider c = - b as Real ;
( |.(|.a.| - |.c.|).| = |.(a + c).| iff |.(a - c).| = |.a.| + |.c.| ) by LmABS;
hence ( |.(a + b).| = |.a.| + |.b.| iff |.(a - b).| = |.(|.a.| - |.b.|).| ) by COMPLEX1:52; :: thesis: verum