let V be RealLinearSpace; :: thesis: for M being non empty Subset of V
for L1, L2 being Convex_Combination of M
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M
let M be non empty Subset of V; :: thesis: for L1, L2 being Convex_Combination of M
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M
let L1, L2 be Convex_Combination of M; :: thesis: for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M
let r be Real; :: thesis: ( 0 < r & r < 1 implies (r * L1) + ((1 - r) * L2) is Convex_Combination of M )
assume A1: ( 0 < r & r < 1 ) ; :: thesis: (r * L1) + ((1 - r) * L2) is Convex_Combination of M
A2: r * L1 is Linear_Combination of M by RLVECT_2:67;
(1 - r) * L2 is Linear_Combination of M by RLVECT_2:67;
hence (r * L1) + ((1 - r) * L2) is Convex_Combination of M by A1, A2, Th9, RLVECT_2:59; :: thesis: verum