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 A is linearly-independent holds
ex I being Basis of V st A c= I
let V be LeftMod of GF; :: thesis: for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
let A be Subset of V; :: thesis: ( A is linearly-independent implies ex I being Basis of V st A c= I )
assume A is linearly-independent ; :: thesis: ex I being Basis of V st A c= I
then consider B being Subset of V such that
A1: A c= B and
A2: B is base by Th17;
reconsider B = B as Basis of V by A2;
take B ; :: thesis: A c= B
thus A c= B by A1; :: thesis: verum