let n be Nat; :: thesis: for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|
let p1, p2, p3 be Element of n -tuples_on REAL; :: thesis: |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|
|((p1 - p2),p3)| = |(p1,p3)| + |((- p2),p3)| by Th130
.= |(p1,p3)| + (- |(p2,p3)|) by Th132 ;
hence |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| ; :: thesis: verum