let x be object ; :: thesis: for GF being Ring
for V being LeftMod of GF
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let GF be Ring; :: thesis: for V being LeftMod of GF
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let V be LeftMod of GF; :: thesis: for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let A be Subset of V; :: thesis: ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
thus ( x in Lin A implies ex l being Linear_Combination of A st x = Sum l ) :: thesis: ( ex l being Linear_Combination of A st x = Sum l implies x in Lin A )

proof

assume x in Lin A ; :: thesis: ex l being Linear_Combination of A st x = Sum l
then x in the carrier of (Lin A) by STRUCT_0:def 5;
then x in { (Sum l) where l is Linear_Combination of A : verum } by Def2;
hence ex l being Linear_Combination of A st x = Sum l ; :: thesis: verum

end;

given k being Linear_Combination of A such that A1: x = Sum k ; :: thesis: x in Lin A
x in { (Sum l) where l is Linear_Combination of A : verum } by A1;
then x in the carrier of (Lin A) by Def2;
hence x in Lin A by STRUCT_0:def 5; :: thesis: verum