theorem Th131: :: RVSUM_1:131

for n being Nat
for p1, p2 being Element of n -tuples_on REAL
for x being Real holds |((x * p1),p2)| = x * |(p1,p2)|