set V = VecSp (K,E);
H0: ( the carrier of (VecSp (K,E)) = the carrier of K & the carrier of (VecSp (E,F)) = the carrier of E ) by FIELD_4:def 6;
defpred S₁[ Element of K, Element of E] means ( ( $1 in BK & $2 = Sum (down (l,$1)) ) or ( not $1 in BK & $2 = 0. E ) );

G0: now :: thesis: for x being Element of K ex y being Element of E st S₁[x,y]

let x be Element of K; :: thesis: ex y being Element of E st S₁[y,b₂]

per cases ( x in BK or not x in BK ) ;

suppose x in BK ; :: thesis: ex y being Element of E st S₁[y,b₂]

hence ex y being Element of E st S₁[x,y] by H0; :: thesis: verum

end;

suppose not x in BK ; :: thesis: ex y being Element of E st S₁[y,b₂]

hence ex y being Element of E st S₁[x,y] ; :: thesis: verum

end;

end;

end;

consider f being Function of the carrier of K, the carrier of E such that
G1: for x being Element of K holds S₁[x,f . x] from FUNCT_2:sch 3(G0);
( dom f = the carrier of (VecSp (K,E)) & rng f c= the carrier of E ) by H0, FUNCT_2:def 1;
then reconsider f = f as Element of Funcs ( the carrier of (VecSp (K,E)), the carrier of E) by FUNCT_2:def 2;
for v being Element of (VecSp (K,E)) st not v in BK holds
f . v = 0. E by H0, G1;
then reconsider l1 = f as Linear_Combination of VecSp (K,E) by VECTSP_6:def 1;

now :: thesis: for o being object st o in Carrier l1 holds
o in BK

let o be object ; :: thesis: ( o in Carrier l1 implies o in BK )
assume C1: o in Carrier l1 ; :: thesis: o in BK
then reconsider v = o as Element of (VecSp (K,E)) ;
l1 . v <> 0. E by C1, VECTSP_6:2;
hence o in BK by H0, G1; :: thesis: verum

end;

then Carrier l1 c= BK ;
then reconsider l1 = l1 as Linear_Combination of BK by VECTSP_6:def 4;
take l1 ; :: thesis: for b being Element of K st b in BK holds
l1 . b = Sum (down (l,b))
thus for b being Element of K st b in BK holds
l1 . b = Sum (down (l,b)) by G1; :: thesis: verum