theorem :: EUCLID_8:68

for r being Real
for p1, p2 being Element of REAL 3 holds |((r * p1),p2)| = r * |(p1,p2)| by RVSUM_1:131;