let n be Nat; :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
let p1, p2, q1, q2 be Point of (TOP-REAL n); :: thesis: |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
A1: |((p1 + p2),q1)| = |(p1,q1)| + |(p2,q1)| by Th40;
A2: |((p1 + p2),q2)| = |(p1,q2)| + |(p2,q2)| by Th40;
|((p1 + p2),(q1 + q2))| = |((p1 + p2),q1)| + |((p1 + p2),q2)| by Th40
.= ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| by A1, A2 ;
hence |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| ; :: thesis: verum