let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n holds |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
let x1, x2, x3 be Element of REAL n; :: thesis: |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
A1: len x3 = n by CARD_1:def 7;
( len x1 = n & len x2 = n ) by CARD_1:def 7;
hence |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| by A1, RVSUM_1:124; :: thesis: verum