let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for V being Subset of (TOP-REAL n) st V = RN_Base n holds
ex l being Linear_Combination of V st p = Sum l
let p be Point of (TOP-REAL n); :: thesis: for V being Subset of (TOP-REAL n) st V = RN_Base n holds
ex l being Linear_Combination of V st p = Sum l
let V be Subset of (TOP-REAL n); :: thesis: ( V = RN_Base n implies ex l being Linear_Combination of V st p = Sum l )
assume A1: V = RN_Base n ; :: thesis: ex l being Linear_Combination of V st p = Sum l
reconsider p0 = p as Element of (RealVectSpace (Seg n)) by Lm1;
reconsider V0 = V as Subset of (RealVectSpace (Seg n)) by Lm1;
consider l0 being Linear_Combination of V0 such that
A2: p0 = Sum l0 by A1, EUCLID_7:43;
reconsider l = l0 as Linear_Combination of TOP-REAL n by Th17;
Carrier l0 c= V0 by RLVECT_2:def 6;
then reconsider l = l as Linear_Combination of V by RLVECT_2:def 6;
take l ; :: thesis: p = Sum l
thus p = Sum l by A2, Th20; :: thesis: verum