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_{1}[x] ) )
from XBOOLE_0:sch 1();

take A ; :: thesis: for L being object holds

( L in A iff L is Linear_Combination of M )

let L be object ; :: thesis: ( L in A iff L is Linear_Combination of M )

thus ( L in A implies L is Linear_Combination of M ) by A1; :: thesis: ( L is Linear_Combination of M implies L in A )

assume L is Linear_Combination of M ; :: thesis: L in A

hence L in A by A1; :: thesis: verum

A1: for x being object holds

( x in A iff ( x in Funcs ( the carrier of V,REAL) & S

take A ; :: thesis: for L being object holds

( L in A iff L is Linear_Combination of M )

let L be object ; :: thesis: ( L in A iff L is Linear_Combination of M )

thus ( L in A implies L is Linear_Combination of M ) by A1; :: thesis: ( L is Linear_Combination of M implies L in A )

assume L is Linear_Combination of M ; :: thesis: L in A

hence L in A by A1; :: thesis: verum