let n be Nat; :: thesis: for a, b being real number
for x1, x2, x3 being Element of REAL n holds |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)
let a, b be real number ; :: thesis: for x1, x2, x3 being Element of REAL n holds |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)
let x1, x2, x3 be Element of REAL n; :: thesis: |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)
thus |(((a * x1) + (b * x2)),x3)| = |((a * x1),x3)| + |((b * x2),x3)| by Th25
.= (a * |(x1,x3)|) + |((b * x2),x3)| by Th26
.= (a * |(x1,x3)|) + (b * |(x2,x3)|) by Th26 ; :: thesis: verum