let n be Nat; 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; |((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; verum