let GF be Ring; :: thesis: for V being LeftMod of GF
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
let V be LeftMod of GF; :: thesis: for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
let A, B be Subset of V; :: thesis: ( A c= B implies Lin A is Subspace of Lin B )
assume A1: A c= B ; :: thesis: Lin A is Subspace 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 Th7;
reconsider l = l as Linear_Combination of B by A1, VECTSP_6:4;
Sum l = v by A2;
hence v in Lin B by Th7; :: thesis: verum
end;
hence Lin A is Subspace of Lin B by VECTSP_4:28; :: thesis: verum