let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds |((- x1),(- x2))| = |(x1,x2)|
let x1, x2 be Element of REAL n; :: thesis: |((- x1),(- x2))| = |(x1,x2)|
thus |((- x1),(- x2))| = - |(x1,(- x2))| by Th23
.= (- 1) * |(x1,(- x2))|
.= (- 1) * (- |(x1,x2)|) by Th23
.= |(x1,x2)| ; :: thesis: verum