let V be Z_Module; :: thesis: for W being Submodule of V
for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let W be Submodule of V; :: thesis: for A being Subset of V st A is linearly-independent & A c= the carrier of W holds
A is linearly-independent Subset of W
let A be Subset of V; :: thesis: ( A is linearly-independent & A c= the carrier of W implies A is linearly-independent Subset of W )
assume that
A1: A is linearly-independent and
A2: A c= the carrier of W ; :: thesis: A is linearly-independent Subset of W
reconsider A9 = A as Subset of W by A2;

now :: thesis: not A9 is linearly-dependent

assume A9 is linearly-dependent ; :: thesis: contradiction
then consider K being Linear_Combination of A9 such that
A3: Sum K = 0. W and
A4: Carrier K <> {} ;
consider L being Linear_Combination of V such that
A5: Carrier L = Carrier K and
A6: Sum L = Sum K by Th12;
reconsider L = L as Linear_Combination of A by A5, VECTSP_6:def 4;
Sum L = 0. V by A3, A6, ZMODUL01:26;
hence contradiction by A1, A4, A5; :: thesis: verum

end;

hence A is linearly-independent Subset of W ; :: thesis: verum