let n be Nat; :: thesis: 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 )
let Af be Subset of (n -VectSp_over F_Real); :: thesis: for Ar being Subset of (REAL-NS n) st Af = Ar holds
( Af is linearly-independent iff Ar is linearly-independent )
let Ar be Subset of (REAL-NS n); :: thesis: ( Af = Ar implies ( Af is linearly-independent iff Ar is linearly-independent ) )
assume A1: Af = Ar ; :: thesis: ( Af is linearly-independent iff Ar is linearly-independent )
reconsider At = Ar as Subset of (TOP-REAL n) by Th4;
( Ar is linearly-independent iff At is linearly-independent ) by Th28;
hence ( Af is linearly-independent iff Ar is linearly-independent ) by A1, MATRTOP2:7; :: thesis: verum