let V be RealLinearSpace; :: thesis: for p, q being Element of V
for a, a1, b1 being Real holds ((a * a1) * p) + ((a * b1) * q) = a * ((a1 * p) + (b1 * q))
let p, q be Element of V; :: thesis: for a, a1, b1 being Real holds ((a * a1) * p) + ((a * b1) * q) = a * ((a1 * p) + (b1 * q))
let a, a1, b1 be Real; :: thesis: ((a * a1) * p) + ((a * b1) * q) = a * ((a1 * p) + (b1 * q))
thus ((a * a1) * p) + ((a * b1) * q) = (a * (a1 * p)) + ((a * b1) * q) by RLVECT_1:def 7
.= (a * (a1 * p)) + (a * (b1 * q)) by RLVECT_1:def 7
.= a * ((a1 * p) + (b1 * q)) by RLVECT_1:def 5 ; :: thesis: verum