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

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