let n be Nat; :: thesis: for x, y being Real
for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
let x, y be Real; :: thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
let p1, p2, p3 be Point of (TOP-REAL n); :: thesis: |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
|(((x * p1) + (y * p2)),p3)| = |((x * p1),p3)| + |((y * p2),p3)| by Th16
.= (x * |(p1,p3)|) + |((y * p2),p3)| by Th17
.= (x * |(p1,p3)|) + (y * |(p2,p3)|) by Th17 ;
hence |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) ; :: thesis: verum