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