let K be Ring; :: thesis: for V being LeftMod of K
for A being Subset of V st 0. V in A & A is linearly-closed holds
A = [#] (Lin A)
let V be LeftMod of K; :: thesis: for A being Subset of V st 0. V in A & A is linearly-closed holds
A = [#] (Lin A)
let A be Subset of V; :: thesis: ( 0. V in A & A is linearly-closed implies A = [#] (Lin A) )
assume A1: ( 0. V in A & A is linearly-closed ) ; :: thesis: A = [#] (Lin A)
thus A c= [#] (Lin A) by Th11; :: according to XBOOLE_0:def 10 :: thesis: [#] (Lin A) c= A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (Lin A) or x in A )
assume x in [#] (Lin A) ; :: thesis: x in A
then x in Lin A ;
then ex l being Linear_Combination of A st x = Sum l by MOD_3:4;
hence x in A by A1, Th12; :: thesis: verum