let a, b1, b2, b3 be Real; for n being Nat
for x1, x2, x3 being Element of REAL n holds a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3)
let n be Nat; for x1, x2, x3 being Element of REAL n holds a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3)
let x1, x2, x3 be Element of REAL n; a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) = (((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3)
thus a * (((b1 * x1) + (b2 * x2)) + (b3 * x3)) =
((a * (b1 * x1)) + (a * (b2 * x2))) + (a * (b3 * x3))
by Th20
.=
(((a * b1) * x1) + (a * (b2 * x2))) + (a * (b3 * x3))
by EUCLID_4:4
.=
(((a * b1) * x1) + ((a * b2) * x2)) + (a * (b3 * x3))
by EUCLID_4:4
.=
(((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3)
by EUCLID_4:4
; verum