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