let V be RealLinearSpace; :: thesis: for v, w, u being Element of V
for a, b, c, d being Real holds a * (((b * v) + (c * w)) + (d * u)) = (((a * b) * v) + ((a * c) * w)) + ((a * d) * u)
let v, w, u be Element of V; :: thesis: for a, b, c, d being Real holds a * (((b * v) + (c * w)) + (d * u)) = (((a * b) * v) + ((a * c) * w)) + ((a * d) * u)
let a, b, c, d be Real; :: thesis: a * (((b * v) + (c * w)) + (d * u)) = (((a * b) * v) + ((a * c) * w)) + ((a * d) * u)
thus (((a * b) * v) + ((a * c) * w)) + ((a * d) * u) = ((a * (b * v)) + ((a * c) * w)) + ((a * d) * u) by RLVECT_1:def 9
.= ((a * (b * v)) + (a * (c * w))) + ((a * d) * u) by RLVECT_1:def 9
.= (a * ((b * v) + (c * w))) + ((a * d) * u) by RLVECT_1:def 9
.= (a * ((b * v) + (c * w))) + (a * (d * u)) by RLVECT_1:def 9
.= a * (((b * v) + (c * w)) + (d * u)) by RLVECT_1:def 9 ; :: thesis: verum