let u, v be VECTOR of V; :: thesis: for p being Real st 0 < p & p < 1 & u in r * M & v in r * M holds
(p * u) + ((1 - p) * v) in r * M
let p be Real; :: thesis: ( 0 < p & p < 1 & u in r * M & v in r * M implies (p * u) + ((1 - p) * v) in r * M )
assume that
A2: ( 0 < p & p < 1 ) and
A3: u in r * M and
A4: v in r * M ; :: thesis: (p * u) + ((1 - p) * v) in r * M
consider v9 being Element of V such that
A5: v = r * v9 and
A6: v9 in M by A4;
consider u9 being Element of V such that
A7: u = r * u9 and
A8: u9 in M by A3;
A9: (p * u) + ((1 - p) * v) = ((r * p) * u9) + ((1 - p) * (r * v9)) by A7, A5, RLVECT_1:def 7
.= ((r * p) * u9) + ((r * (1 - p)) * v9) by RLVECT_1:def 7
.= (r * (p * u9)) + ((r * (1 - p)) * v9) by RLVECT_1:def 7
.= (r * (p * u9)) + (r * ((1 - p) * v9)) by RLVECT_1:def 7
.= r * ((p * u9) + ((1 - p) * v9)) by RLVECT_1:def 5 ;
(p * u9) + ((1 - p) * v9) in M by A1, A2, A8, A6;
hence (p * u) + ((1 - p) * v) in r * M by A9; :: thesis: verum