let p1, p2, q1, q2 be Element of REAL 3; :: thesis: |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
A1: |((p1 + p2),(q1 + q2))| = |(p1,(q1 + q2))| + |(p2,(q1 + q2))| by Th75;
A2: |(p1,(q1 + q2))| = |(p1,q1)| + |(p1,q2)| by Th75;
|(p2,(q1 + q2))| = |(p2,q1)| + |(p2,q2)| by Th75;
hence |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| by A1, A2; :: thesis: verum