theorem :: EUCLID_8:82

for p, q being Element of REAL 3 holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| by RVSUM_1:138;