theorem :: EUCLID_8:76

for r1, r2 being Real
for q, p1, p2 being Element of REAL 3 holds |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|) by RVSUM_1:135;