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