consider A being set such that
A1: for x being object 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 object holds
( L in A iff L is Convex_Combination of V )
let L be object ; :: thesis: ( L in A iff L is Convex_Combination of V )
thus ( L in A implies L is Convex_Combination of V ) by A1; :: thesis: ( L is Convex_Combination of V implies L in A )
assume L is Convex_Combination of V ; :: thesis: L in A
hence L in A by A1; :: thesis: verum