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