let p, q be Element of REAL 3; :: thesis: |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|
|((p + q),(p + q))| = ((|(p,p)| + |(p,q)|) + |(q,p)|) + |(q,q)| by Th77;
hence |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| ; :: thesis: verum