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)|
( len x1 = n & len x2 = n ) by FINSEQ_1:def 18;
hence |((- x1),x2)| = - |(x1,x2)| by EUCLID_2:22; :: thesis: verum