let V be RealLinearSpace; :: thesis: for o, u, v1, w1, u2 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 o, u, v1, w1, u2 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 3 ;
:: thesis: verum