let V be RealLinearSpace; :: thesis: for o, p, q, r being Element of V
for a, b being Real st r = (a * p) + (b * q) holds
r = ((0 * o) + (a * p)) + (b * q)
let o, p, q, r be Element of V; :: thesis: for a, b being Real st r = (a * p) + (b * q) holds
r = ((0 * o) + (a * p)) + (b * q)
let a, b be Real; :: thesis: ( r = (a * p) + (b * q) implies r = ((0 * o) + (a * p)) + (b * q) )
assume r = (a * p) + (b * q) ; :: thesis: r = ((0 * o) + (a * p)) + (b * q)
hence r = ((0. V) + (a * p)) + (b * q) by RLVECT_1:4
.= ((0 * o) + (a * p)) + (b * q) by RLVECT_1:10 ;
:: thesis: verum