theorem Th19: :: VECTSP_9:19

for GF being Field
for V being VectSp of GF
for A, B being finite Subset of V st ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin A & B is linearly-independent holds
( card B <= card A & ex C being finite Subset of V st
( C c= A & card C = (card A) - (card B) & ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = Lin (B \/ C) ) )