let n be Nat; :: thesis: for p1, p2 being Element of n -tuples_on REAL holds |((- p1),(- p2))| = |(p1,p2)|
let p1, p2 be Element of n -tuples_on REAL; :: thesis: |((- p1),(- p2))| = |(p1,p2)|
|((- p1),(- p2))| = - |(p1,(- p2))| by Th132
.= - (- |(p1,p2)|) by Th132 ;
hence |((- p1),(- p2))| = |(p1,p2)| ; :: thesis: verum