set S = { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) } ;
take { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) } ; :: thesis: for x being object holds
( x in { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict free Submodule of V st
( W = x & rank W = n ) )
for x being object holds
( x in { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict free Submodule of V st
( W = x & rank W = n ) )

proof

let x be object ; :: thesis: ( x in { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict free Submodule of V st
( W = x & rank W = n ) )

hereby :: thesis: ( ex W being strict free Submodule of V st
( W = x & rank W = n ) implies x in { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) } )

assume x in { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) } ; :: thesis: ex W being strict free Submodule of V st
( W = x & rank W = n )
then A1: ex A being finite Subset of V st
( x = Lin A & A is linearly-independent & card A = n ) ;
then reconsider W = x as strict free Submodule of V ;
rank W = n by A1, RL5Th30;
hence ex W being strict free Submodule of V st
( W = x & rank W = n ) ; :: thesis: verum

end;

given W being strict free Submodule of V such that A2: W = x and
A3: rank W = n ; :: thesis: x in { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) }
consider A being finite Subset of W such that
A4: A is Basis of W by ZMODUL03:def 3;
reconsider A = A as Subset of W ;
reconsider B = A as linearly-independent Subset of V by A4, ZMODUL03:15, VECTSP_7:def 3;
A5: x = Lin A by A2, A4, VECTSP_7:def 3
.= Lin B by ZMODUL03:20 ;
then card B = n by A2, A3, RL5Th30;
hence x in { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) } by A5; :: thesis: verum

end;

hence for x being object holds
( x in { (Lin A) where A is finite Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict free Submodule of V st
( W = x & rank W = n ) ) ; :: thesis: verum