defpred S_{1}[ object ] means $1 is Linear_Combination of V;

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 x being set holds

( x in A iff x is Linear_Combination of V )

let x be set ; :: thesis: ( x in A iff x is Linear_Combination of V )

thus ( x in A implies x is Linear_Combination of V ) by A1; :: thesis: ( x is Linear_Combination of V implies x in A )

assume x is Linear_Combination of V ; :: thesis: x in A

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

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

take A ; :: thesis: for x being set holds

( x in A iff x is Linear_Combination of V )

let x be set ; :: thesis: ( x in A iff x is Linear_Combination of V )

thus ( x in A implies x is Linear_Combination of V ) by A1; :: thesis: ( x is Linear_Combination of V implies x in A )

assume x is Linear_Combination of V ; :: thesis: x in A

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