let T be RealLinearSpace; :: thesis: for X being set holds
( X is Linear_Combination of RLSp2RVSp T iff X is Linear_Combination of T )
let X be set ; :: thesis: ( X is Linear_Combination of RLSp2RVSp T iff X is Linear_Combination of T )
set V = RLSp2RVSp T;
hereby :: thesis: ( X is Linear_Combination of T implies X is Linear_Combination of RLSp2RVSp T )
assume X is Linear_Combination of RLSp2RVSp T ; :: thesis: X is Linear_Combination of T
then reconsider L = X as Linear_Combination of RLSp2RVSp T ;
consider S being finite Subset of (RLSp2RVSp T) such that
A1: for v being Element of (RLSp2RVSp T) st not v in S holds
L . v = 0. F_Real by VECTSP_6:def 1;
thus X is Linear_Combination of T by A1, RLVECT_2:def 3; :: thesis: verum
end;
assume X is Linear_Combination of T ; :: thesis: X is Linear_Combination of RLSp2RVSp T
then reconsider L = X as Linear_Combination of T ;
consider S being finite Subset of T such that
A2: for v being Element of T st not v in S holds
L . v = 0 by RLVECT_2:def 3;
for v being Element of (RLSp2RVSp T) st not v in S holds
0. F_Real = L . v by A2;
hence X is Linear_Combination of RLSp2RVSp T by VECTSP_6:def 1; :: thesis: verum