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:
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 ;
Sum L = 0. V by ;
hence contradiction by A1, A4, A5; :: thesis: verum
end;
hence A is linearly-independent Subset of W ; :: thesis: verum