theorem :: REAL_NS2:29

for n being Nat
for Af being Subset of (n -VectSp_over F_Real)
for Ar being Subset of (REAL-NS n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )