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 S₁[ 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 ) );

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

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

per cases ( ( x in BE & b in BK ) or not x in BE or not b in BK ) ;

suppose G: ( x in BE & b in BK ) ; :: thesis: ex y being Element of F st S₁[y,b₂]

thus ex y being Element of F st S₁[x,y] :: thesis: verum

proof

take l . ((@ (x,K)) * b) ; :: thesis: ( l . ((@ (x,K)) * b) is Element of F & S₁[x,l . ((@ (x,K)) * b)] )
thus ( l . ((@ (x,K)) * b) is Element of F & S₁[x,l . ((@ (x,K)) * b)] ) by G, H0, FUNCT_2:5; :: thesis: verum

end;

end;

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

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

end;

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

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

end;

end;

end;

consider f being Function of the carrier of E, the carrier of F such that
G1: for x being Element of E holds S₁[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;

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

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

end;

then Carrier l1 c= BE ;
then reconsider l1 = l1 as Linear_Combination of BE by VECTSP_6:def 4;
take l1 ; :: thesis: ( ( 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 ) )

now :: thesis: for a being Element of K st a in BE & b in BK holds
l1 . a = l . (a * b)

let a be Element of K; :: thesis: ( a in BE & b in BK implies l1 . a = l . (a * b) )
assume G: ( a in BE & b in BK ) ; :: thesis: l1 . a = l . (a * b)
then reconsider aE = a as Element of E by FIELD_4:def 6;
thus l1 . a = l . ((@ (aE,K)) * b) by G, G1
.= l . (a * b) ; :: thesis: verum

end;

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; :: thesis: verum