let GF be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for V being LeftMod of GF
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
let V be LeftMod of GF; :: thesis: for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
let A be Subset of V; :: thesis: ( Lin A = V implies ex I being Basis of V st I c= A )
assume Lin A = V ; :: thesis: ex I being Basis of V st I c= A
then consider B being Subset of V such that
A1: B c= A and
A2: ( B is linearly-independent & Lin B = V ) by Th18;
reconsider B = B as Basis of V by A2, Def3;
take B ; :: thesis: B c= A
thus B c= A by A1; :: thesis: verum