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