let r1, r2 be Element of REAL ; :: thesis: for p1, p2, q being Element of REAL 3 holds |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|)
let p1, p2, q be Element of REAL 3; :: thesis: |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|)
|(((r1 * p1) + (r2 * p2)),q)| = |((r1 * p1),q)| + |((r2 * p2),q)| by Th75;
then |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + |((r2 * p2),q)| by Th68;
hence |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|) by Th68; :: thesis: verum