theorem Th21: :: MFOLD_2:21

for n being Nat
for Af being Subset of (RealVectSpace (Seg n))
for Ar being Subset of (TOP-REAL n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )