let T be RealLinearSpace; :: thesis: for X being set
for U being Subspace of RLSp2RVSp T
for W being Subspace of T st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
let X be set ; :: thesis: for U being Subspace of RLSp2RVSp T
for W being Subspace of T st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
let U be Subspace of RLSp2RVSp T; :: thesis: for W being Subspace of T st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
let W be Subspace of T; :: thesis: ( [#] U = [#] W implies ( X is Linear_Combination of U iff X is Linear_Combination of W ) )
assume A1: [#] U = [#] W ; :: thesis: ( X is Linear_Combination of U iff X is Linear_Combination of W )

hereby :: thesis: ( X is Linear_Combination of W implies X is Linear_Combination of U )

assume X is Linear_Combination of U ; :: thesis: X is Linear_Combination of W
then reconsider L = X as Linear_Combination of U ;
ex S being finite Subset of U st
for v being Element of U st not v in S holds
L . v = 0. F_Real by VECTSP_6:def 1;
hence X is Linear_Combination of W by A1, RLVECT_2:def 3; :: thesis: verum

end;

assume X is Linear_Combination of W ; :: thesis: X is Linear_Combination of U
then reconsider L = X as Linear_Combination of W ;
consider S being finite Subset of W such that
A2: for v being Element of W st not v in S holds
L . v = 0 by RLVECT_2:def 3;
for v being Element of U st not v in S holds
0. F_Real = L . v by A1, A2;
hence X is Linear_Combination of U by A1, VECTSP_6:def 1; :: thesis: verum