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;

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

hence
A is linearly-independent Subset of W
; :: thesis: verumassume
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;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