let n be Nat; :: thesis: for a, b being Real
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; :: 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 Th20
.= (a * |(x1,x3)|) + |((b * x2),x3)| by Th21
.= (a * |(x1,x3)|) + (b * |(x2,x3)|) by Th21 ; :: thesis: verum