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

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