theorem :: RVSUM_1:140

for n being Nat
for p, q being Element of n -tuples_on REAL holds |(p,q)| <= |(p,p)| + |(q,q)|