consider A being set such that
A1: for x being set holds
( x in A iff ( x in Funcs the carrier of V,REAL & S₁[x] ) ) from XBOOLE_0:sch 1();
take A ; :: thesis: for L being set holds
( L in A iff L is Convex_Combination of )
let L be set ; :: thesis: ( L in A iff L is Convex_Combination of )
thus ( L in A implies L is Convex_Combination of ) by A1; :: thesis: ( L is Convex_Combination of implies L in A )
assume L is Convex_Combination of ; :: thesis: L in A
hence L in A by A1; :: thesis: verum