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