let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let A, B be Subset of V; :: thesis: ( A c= B & B is linearly-independent implies A is linearly-independent )
assume that
A1: A c= B and
A2: B is linearly-independent ; :: thesis: A is linearly-independent
let l be Linear_Combination of A; :: according to VECTSP_7:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
reconsider L = l as Linear_Combination of B by A1, VECTSP_6:4;
assume Sum l = 0. V ; :: thesis: Carrier l = {}
then Carrier L = {} by A2;
hence Carrier l = {} ; :: thesis: verum