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 )
A1: ( r * L1 is Linear_Combination of M & (1 - r) * L2 is Linear_Combination of M ) by RLVECT_2:44;
assume ( 0 < r & r < 1 ) ; :: thesis: (r * L1) + ((1 - r) * L2) is Convex_Combination of M
hence (r * L1) + ((1 - r) * L2) is Convex_Combination of M by A1, Th8, RLVECT_2:38; :: thesis: verum