let V be RealLinearSpace; :: thesis: for o, r, u, v, u2, v2 being Element of V
for a1, a2, A, B being Real st r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) holds
r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)
let o, r, u, v, u2, v2 be Element of V; :: thesis: for a1, a2, A, B being Real st r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) holds
r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)
let a1, a2 be Real; :: thesis: for A, B being Real st r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) holds
r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)
let A, B be Real; :: thesis: ( r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) implies r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v) )
assume ( r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) ) ; :: thesis: r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)
hence r = ((A * o) + (A * (a1 * u))) + (B * (o + (a2 * v))) by RLVECT_1:def 5
.= ((A * o) + (A * (a1 * u))) + ((B * o) + (B * (a2 * v))) by RLVECT_1:def 5
.= ((A * o) + ((A * a1) * u)) + ((B * o) + (B * (a2 * v))) by RLVECT_1:def 7
.= ((A * o) + ((A * a1) * u)) + ((B * o) + ((B * a2) * v)) by RLVECT_1:def 7
.= (((A * o) + ((A * a1) * u)) + (B * o)) + ((B * a2) * v) by RLVECT_1:def 3
.= (((A * o) + (B * o)) + ((A * a1) * u)) + ((B * a2) * v) by RLVECT_1:def 3
.= (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v) by RLVECT_1:def 6 ;
:: thesis: verum