theorem Th78: :: REAL_NS2:78

for T being RealLinearSpace
for Af being Subset of (RLSp2RVSp T)
for Ar being Subset of T st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )