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

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