theorem Th25: :: REAL_NS2:25

for n being Nat
for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n) st Ar = At holds
for X being object holds
( X is Linear_Combination of Ar iff X is Linear_Combination of At )