let x be object ; :: thesis: for V being RealLinearSpace

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 RealLinearSpace; :: 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 )

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

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 RealLinearSpace; :: 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

given k being Linear_Combination of A such that A1:
x = Sum k
; :: thesis: x in Lin A
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;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

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