set V = VecSp (E,F);
H0:
( the carrier of (VecSp (E,F)) = the carrier of E & the carrier of (VecSp (K,F)) = the carrier of K )
by FIELD_4:def 6;
defpred S1[ Element of E, Element of F] means ( ( $1 in BE & b in BK & $2 = l . ((@ ($1,K)) * b) ) or ( ( not $1 in BE or not b in BK ) & $2 = 0. F ) );
consider f being Function of the carrier of E, the carrier of F such that
G1:
for x being Element of E holds S1[x,f . x]
from FUNCT_2:sch 3(G0);
( dom f = the carrier of (VecSp (E,F)) & rng f c= the carrier of F )
by H0, FUNCT_2:def 1;
then reconsider f = f as Element of Funcs ( the carrier of (VecSp (E,F)), the carrier of F) by FUNCT_2:def 2;
for v being Element of (VecSp (E,F)) st not v in BE holds
f . v = 0. F
by H0, G1;
then reconsider l1 = f as Linear_Combination of VecSp (E,F) by VECTSP_6:def 1;
then
Carrier l1 c= BE
;
then reconsider l1 = l1 as Linear_Combination of BE by VECTSP_6:def 4;
take
l1
; ( ( for a being Element of K st a in BE & b in BK holds
l1 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
l1 . a = 0. F ) )
hence
( ( for a being Element of K st a in BE & b in BK holds
l1 . a = l . (a * b) ) & ( for a being Element of E st ( not a in BE or not b in BK ) holds
l1 . a = 0. F ) )
by G1; verum