let V be Z_Module; :: thesis: for W being Submodule of V

for A being Subset of V st A c= the carrier of W holds

Lin A is Submodule of W

let W be Submodule of V; :: thesis: for A being Subset of V st A c= the carrier of W holds

Lin A is Submodule of W

let A be Subset of V; :: thesis: ( A c= the carrier of W implies Lin A is Submodule of W )

assume A1: A c= the carrier of W ; :: thesis: Lin A is Submodule of W

for A being Subset of V st A c= the carrier of W holds

Lin A is Submodule of W

let W be Submodule of V; :: thesis: for A being Subset of V st A c= the carrier of W holds

Lin A is Submodule of W

let A be Subset of V; :: thesis: ( A c= the carrier of W implies Lin A is Submodule of W )

assume A1: A c= the carrier of W ; :: thesis: Lin A is Submodule of W

now :: thesis: for w being object st w in the carrier of (Lin A) holds

w in the carrier of W

hence
Lin A is Submodule of W
by TARSKI:def 3, ZMODUL01:43; :: thesis: verumw in the carrier of W

let w be object ; :: thesis: ( w in the carrier of (Lin A) implies w in the carrier of W )

assume w in the carrier of (Lin A) ; :: thesis: w in the carrier of W

then consider L being Linear_Combination of A such that

A2: w = Sum L by STRUCT_0:def 5, ZMODUL02:64;

Carrier L c= A by VECTSP_6:def 4;

then ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum L = Sum K ) by A1, Th13, XBOOLE_1:1;

hence w in the carrier of W by A2; :: thesis: verum

end;assume w in the carrier of (Lin A) ; :: thesis: w in the carrier of W

then consider L being Linear_Combination of A such that

A2: w = Sum L by STRUCT_0:def 5, ZMODUL02:64;

Carrier L c= A by VECTSP_6:def 4;

then ex K being Linear_Combination of W st

( Carrier K = Carrier L & Sum L = Sum K ) by A1, Th13, XBOOLE_1:1;

hence w in the carrier of W by A2; :: thesis: verum