let V be RealLinearSpace; :: thesis: for p, q, r, w, y being Element of V
for a, b, c, a1, b1 being Real st y = (a1 * p) + (b1 * w) & w = ((a * p) + (b * q)) + (c * r) holds
y = (((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r)
let p, q, r, w, y be Element of V; :: thesis: for a, b, c, a1, b1 being Real st y = (a1 * p) + (b1 * w) & w = ((a * p) + (b * q)) + (c * r) holds
y = (((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r)
let a, b, c, a1, b1 be Real; :: thesis: ( y = (a1 * p) + (b1 * w) & w = ((a * p) + (b * q)) + (c * r) implies y = (((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r) )
assume ( y = (a1 * p) + (b1 * w) & w = ((a * p) + (b * q)) + (c * r) ) ; :: thesis: y = (((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r)
hence y = (a1 * p) + ((((b1 * a) * p) + ((b1 * b) * q)) + ((b1 * c) * r)) by Lm6
.= (a1 * p) + (((b1 * a) * p) + (((b1 * b) * q) + ((b1 * c) * r))) by RLVECT_1:def 3
.= ((a1 * p) + ((b1 * a) * p)) + (((b1 * b) * q) + ((b1 * c) * r)) by RLVECT_1:def 3
.= ((a1 + (b1 * a)) * p) + (((b1 * b) * q) + ((b1 * c) * r)) by RLVECT_1:def 6
.= (((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r) by RLVECT_1:def 3 ;
:: thesis: verum