let x, y be VECTOR of V; :: thesis: for a being Real st x in v + M & y in v + M holds
((1 - a) * x) + (a * y) in v + M
let a be Real; :: thesis: ( x in v + M & y in v + M implies ((1 - a) * x) + (a * y) in v + M )
assume that
A1: x in v + M and
A2: y in v + M ; :: thesis: ((1 - a) * x) + (a * y) in v + M
consider x9 being Element of V such that
A3: x = v + x9 and
A4: x9 in M by A1;
consider y9 being Element of V such that
A5: y = v + y9 and
A6: y9 in M by A2;
A7: ((1 - a) * x) + (a * y) = (((1 - a) * v) + ((1 - a) * x9)) + (a * (v + y9)) by A3, A5, RLVECT_1:def 5
.= (((1 - a) * v) + ((1 - a) * x9)) + ((a * v) + (a * y9)) by RLVECT_1:def 5
.= ((((1 - a) * v) + ((1 - a) * x9)) + (a * v)) + (a * y9) by RLVECT_1:def 3
.= (((1 - a) * x9) + (((1 - a) * v) + (a * v))) + (a * y9) by RLVECT_1:def 3
.= (((1 - a) * x9) + (((1 - a) + a) * v)) + (a * y9) by RLVECT_1:def 6
.= (((1 - a) * x9) + v) + (a * y9) by RLVECT_1:def 8
.= v + (((1 - a) * x9) + (a * y9)) by RLVECT_1:def 3 ;
((1 - a) * x9) + (a * y9) in M by A4, A6, Def4;
hence ((1 - a) * x) + (a * y) in v + M by A7; :: thesis: verum