theorem Th1: :: MATRTOP2:1

for X being set
for n being Nat holds
( X is Linear_Combination of n -VectSp_over F_Real iff X is Linear_Combination of TOP-REAL n )