theorem Th130: :: RVSUM_1:130

for n being Nat
for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|