let V be RealLinearSpace; :: thesis: for o, u, w1, u2, v2 being Element of V
for a, b, c2 being Real st w1 = (a * u) + (b * v2) & v2 = o + (c2 * u2) holds
w1 = ((b * o) + (a * u)) + ((b * c2) * u2)
let o, u, w1, u2, v2 be Element of V; :: thesis: for a, b, c2 being Real st w1 = (a * u) + (b * v2) & v2 = o + (c2 * u2) holds
w1 = ((b * o) + (a * u)) + ((b * c2) * u2)
let a, b, c2 be Real; :: thesis: ( w1 = (a * u) + (b * v2) & v2 = o + (c2 * u2) implies w1 = ((b * o) + (a * u)) + ((b * c2) * u2) )
assume ( w1 = (a * u) + (b * v2) & v2 = o + (c2 * u2) ) ; :: thesis: w1 = ((b * o) + (a * u)) + ((b * c2) * u2)
hence w1 = (a * u) + ((b * o) + (b * (c2 * u2))) by RLVECT_1:def 5
.= ((a * u) + (b * o)) + (b * (c2 * u2)) by RLVECT_1:def 3
.= ((b * o) + (a * u)) + ((b * c2) * u2) by RLVECT_1:def 7 ;
:: thesis: verum