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