let R be domRing; :: thesis: for V being RightMod of R
for A, B being Subset of V st A c= B holds
Lin A is Submodule of Lin B
let V be RightMod of R; :: thesis: for A, B being Subset of V st A c= B holds
Lin A is Submodule of Lin B
let A, B be Subset of V; :: thesis: ( A c= B implies Lin A is Submodule of Lin B )
assume A1: A c= B ; :: thesis: Lin A is Submodule of Lin B

now :: thesis: for v being Vector of V st v in Lin A holds
v in Lin B

let v be Vector of V; :: thesis: ( v in Lin A implies v in Lin B )
assume v in Lin A ; :: thesis: v in Lin B
then consider l being Linear_Combination of A such that
A2: v = Sum l by Th67;
reconsider l = l as Linear_Combination of B by A1, Th19;
Sum l = v by A2;
hence v in Lin B by Th67; :: thesis: verum

end;

hence Lin A is Submodule of Lin B by RMOD_2:28; :: thesis: verum