theorem :: RVSUM_1:133

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