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
now :: thesis: for w being object st w in the carrier of (Lin A) holds
w 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;
hence Lin A is Submodule of W by TARSKI:def 3, ZMODUL01:43; :: thesis: verum