let n be Nat; 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; 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; |(((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
; verum