let x be object ; :: thesis: for GF being Ring
for V being LeftMod of GF
for A being Subset of V st x in A holds
x in Lin A
let GF be Ring; :: thesis: for V being LeftMod of GF
for A being Subset of V st x in A holds
x in Lin A
let V be LeftMod of GF; :: thesis: for A being Subset of V st x in A holds
x in Lin A
let A be Subset of V; :: thesis: ( x in A implies x in Lin A )
deffunc H₁( set ) -> Element of the carrier of GF = 0. GF;
assume A1: x in A ; :: thesis: x in Lin A
then reconsider v = x as Vector of V ;
consider f being Function of V,GF such that
A2: f . v = 1_ GF and
A3: for u being Vector of V st u <> v holds
f . u = H₁(u) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
ex T being finite Subset of V st
for u being Vector of V st not u in T holds
f . u = 0. GF

proof

take T = {v}; :: thesis: for u being Vector of V st not u in T holds
f . u = 0. GF
let u be Vector of V; :: thesis: ( not u in T implies f . u = 0. GF )
assume not u in T ; :: thesis: f . u = 0. GF
then u <> v by TARSKI:def 1;
hence f . u = 0. GF by A3; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;
A4: Carrier f c= {v}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v} )
assume x in Carrier f ; :: thesis: x in {v}
then consider u being Vector of V such that
A5: x = u and
A6: f . u <> 0. GF ;
u = v by A3, A6;
hence x in {v} by A5, TARSKI:def 1; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of {v} by VECTSP_6:def 4;
A7: Sum f = (1_ GF) * v by A2, VECTSP_6:17
.= v ;
{v} c= A by A1, ZFMISC_1:31;
then Carrier f c= A by A4;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def 4;
Sum f = v by A7;
hence x in Lin A by Th7; :: thesis: verum