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)| = |(((- 1) * p1),p2)|
.= (- 1) * |(p1,p2)| by Th131 ;
hence |((- p1),p2)| = - |(p1,p2)| ; :: thesis: verum