let V be RealLinearSpace; :: thesis: for w1, u2, v1, o, u being Element of V
for a, b, a2 being Real st w1 = (a * u2) + (b * v1) & v1 = o + (a2 * u) holds
w1 = ((b * o) + ((b * a2) * u)) + (a * u2)
let w1, u2, v1, o, u be Element of V; :: thesis: for a, b, a2 being Real st w1 = (a * u2) + (b * v1) & v1 = o + (a2 * u) holds
w1 = ((b * o) + ((b * a2) * u)) + (a * u2)
let a, b, a2 be Real; :: thesis: ( w1 = (a * u2) + (b * v1) & v1 = o + (a2 * u) implies w1 = ((b * o) + ((b * a2) * u)) + (a * u2) )
assume ( w1 = (a * u2) + (b * v1) & v1 = o + (a2 * u) ) ; :: thesis: w1 = ((b * o) + ((b * a2) * u)) + (a * u2)
hence w1 = ((b * o) + (a * u2)) + ((b * a2) * u) by Lm18
.= ((b * o) + ((b * a2) * u)) + (a * u2) by RLVECT_1:def 6 ;
:: thesis: verum