let n be Nat; :: thesis: for X being set
for U being Subspace of REAL-NS n
for W being Subspace of n -VectSp_over F_Real 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 REAL-NS n
for W being Subspace of n -VectSp_over F_Real st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
let U be Subspace of REAL-NS n; :: thesis: for W being Subspace of n -VectSp_over F_Real st [#] U = [#] W holds
( X is Linear_Combination of U iff X is Linear_Combination of W )
let W be Subspace of n -VectSp_over F_Real; :: 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 )
reconsider S = U as Subspace of TOP-REAL n by Th30;
( X is Linear_Combination of S iff X is Linear_Combination of W ) by A1, MATRTOP2:11;
hence ( X is Linear_Combination of U iff X is Linear_Combination of W ) ; :: thesis: verum