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 7

.= (a * (b * v)) + (a * (c * w)) by RLVECT_1:def 7

.= a * ((b * v) + (c * w)) by RLVECT_1:def 5 ; :: thesis: verum

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 7

.= (a * (b * v)) + (a * (c * w)) by RLVECT_1:def 7

.= a * ((b * v) + (c * w)) by RLVECT_1:def 5 ; :: thesis: verum