set S = { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ;

take { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; :: thesis: for x being object holds

( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st

( W = x & dim W = n ) )

for x being object holds

( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st

( W = x & dim W = n ) )

( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ; :: thesis: verum

take { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; :: thesis: for x being object holds

( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st

( W = x & dim W = n ) )

for x being object holds

( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st

( W = x & dim W = n ) )

proof

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

( W = x & dim W = n ) )

A3: dim W = n ; :: thesis: x in { (Lin A) where A is 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 Def1;

reconsider A = A as Subset of W ;

A is linearly-independent by A4, RLVECT_3:def 3;

then reconsider B = A as linearly-independent Subset of V by Th14;

A5: x = Lin A by A2, A4, RLVECT_3:def 3

.= Lin B by Th20 ;

then card B = n by A2, A3, Th29;

hence x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } by A5; :: thesis: verum

end;( W = x & dim W = n ) )

hereby :: thesis: ( ex W being strict Subspace of V st

( W = x & dim W = n ) implies x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } )

given W being strict Subspace of V such that A2:
W = x
and ( W = x & dim W = n ) implies x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } )

assume
x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) }
; :: thesis: ex W being strict Subspace of V st

( W = x & dim W = n )

then A1: ex A being Subset of V st

( x = Lin A & A is linearly-independent & card A = n ) ;

then reconsider W = x as strict Subspace of V ;

dim W = n by A1, Th29;

hence ex W being strict Subspace of V st

( W = x & dim W = n ) ; :: thesis: verum

end;( W = x & dim W = n )

then A1: ex A being Subset of V st

( x = Lin A & A is linearly-independent & card A = n ) ;

then reconsider W = x as strict Subspace of V ;

dim W = n by A1, Th29;

hence ex W being strict Subspace of V st

( W = x & dim W = n ) ; :: thesis: verum

A3: dim W = n ; :: thesis: x in { (Lin A) where A is 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 Def1;

reconsider A = A as Subset of W ;

A is linearly-independent by A4, RLVECT_3:def 3;

then reconsider B = A as linearly-independent Subset of V by Th14;

A5: x = Lin A by A2, A4, RLVECT_3:def 3

.= Lin B by Th20 ;

then card B = n by A2, A3, Th29;

hence x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } by A5; :: thesis: verum

( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ; :: thesis: verum