let F be Field; :: thesis:
let V be VectSp of F; :: thesis:
let W be Subspace of V; :: thesis:
let l1 be Linear_Combination of W; :: thesis:
H: the carrier of W c= the carrier of V by VECTSP_4:def 2;
consider f being Function such that
L1: ( l1 = f & dom f = the carrier of W & rng f c= the carrier of F ) by FUNCT_2:def 2;
reconsider f = f as Function of W,F by L1;
defpred S₁[ Element of V, Element of F] means ( ( $1 in Carrier l1 & $2 = f . $1 ) or ( not $1 in Carrier l1 & $2 = 0. F ) );
A: for x being Element of the carrier of V ex y being Element of the carrier of F st S₁[x,y]

let v be Element of the carrier of V; :: thesis:

then reconsider v1 = v as Element of W ;
reconsider y = f . v1 as Element of F ;
take y ; :: thesis:
thus S₁[v,y] by A1; :: thesis:

end;

end;

consider g being Function of V,F such that
B: for x being Element of V holds S₁[x,g . x] from FUNCT_2:sch 3(A);
( dom g = the carrier of V & rng g c= the carrier of F ) by FUNCT_2:def 1;
then C: g is Element of Funcs ( the carrier of V, the carrier of F) by FUNCT_2:def 2;
for o being object st o in Carrier l1 holds
o in the carrier of V by H;
then reconsider C = Carrier l1 as finite Subset of V by TARSKI:def 3;
for v being Element of V st not v in C holds
g . v = 0. F by B;
then reconsider l2 = g as Linear_Combination of V by C, VECTSP_6:def 1;
take l2 ; :: thesis:

let o be object ; :: thesis:
assume o in Carrier l2 ; :: thesis:
then consider v being Element of V such that
G1: ( o = v & l2 . v <> 0. F ) by VECTSP_6:1;
thus o in Carrier l1 by B, G1; :: thesis:

end;

let o be object ; :: thesis:
assume G0: o in Carrier l1 ; :: thesis:
then consider v being Element of W such that
G1: ( o = v & l1 . v <> 0. F ) by VECTSP_6:1;
reconsider v1 = v as Element of V by H;
( v1 in Carrier l1 & g . v1 = f . v1 ) by B, G1, G0;
hence o in Carrier l2 by L1, G1, VECTSP_6:2; :: thesis:

end;