let V be RealLinearSpace; :: thesis: for w1, u, v2, o, u2 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 w1, u, v2, o, u2 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 9
.= ((a * u) + (b * o)) + (b * (c2 * u2)) by RLVECT_1:def 6
.= ((b * o) + (a * u)) + ((b * c2) * u2) by RLVECT_1:def 9 ;
:: thesis: verum