theorem Th132: :: RVSUM_1:132

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