theorem :: EUCLID_8:75

for q, p1, p2 being Element of REAL 3 holds |((p1 + p2),q)| = |(p1,q)| + |(p2,q)| by RVSUM_1:130;