set V = VecSp (K,F);
H0: ( the carrier of (VecSp (K,F)) = the carrier of K & the carrier of (VecSp (E,F)) = the carrier of E & the carrier of (VecSp (K,E)) = the carrier of K ) by FIELD_4:def 6;
defpred S₁[ Element of K, Element of F] means ( ( $1 in Base (BE,BK) & ex a, b being Element of K st
( $1 = a * b & a in BE & b in BK & a * b in Base (BE,BK) & ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & $2 = l2 . a ) ) ) or ( not $1 in Base (BE,BK) & $2 = 0. F ) );

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

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

per cases ( x in Base (BE,BK) or not x in Base (BE,BK) ) ;

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

then consider a, b being Element of K such that
G1: ( x = a * b & a in BE & b in BK ) ;
consider l2 being Linear_Combination of BE such that
G2: l1 . b = Sum l2 by T0;
reconsider y = l2 . a as Element of F by G1, FUNCT_2:5;
S₁[x,y] by G, G2, G1;
hence ex y being Element of F st S₁[x,y] ; :: thesis: verum

end;

suppose not x in Base (BE,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 K, the carrier of F 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,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 (K,F)), the carrier of F) by FUNCT_2:def 2;
for v being Element of (VecSp (K,F)) st not v in Base (BE,BK) holds
f . v = 0. F by H0, G1;
then reconsider l = f as Linear_Combination of VecSp (K,F) by VECTSP_6:def 1;

now :: thesis: for o being object st o in Carrier l holds
o in Base (BE,BK)

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

end;

then Carrier l c= Base (BE,BK) ;
then reconsider l = l as Linear_Combination of Base (BE,BK) by VECTSP_6:def 4;
take l ; :: thesis: for b being Element of K st b in BK holds
ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
l . (a * b) = l2 . a ) )

now :: thesis: for b being Element of K st b in BK holds
ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
l . (a * b) = l2 . a ) )

let b be Element of K; :: thesis: ( b in BK implies ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
l . (a * b) = l2 . a ) ) )
assume F1: b in BK ; :: thesis: ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
l . (a * b) = l2 . a ) )
consider l2 being Linear_Combination of BE such that
F2: l1 . b = Sum l2 by T0;

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

let a be Element of K; :: thesis: ( a in BE & a * b in Base (BE,BK) implies l . (a * b) = l2 . a )
assume F3: ( a in BE & a * b in Base (BE,BK) ) ; :: thesis: l . (a * b) = l2 . a
reconsider y = l . (a * b) as Element of F by FUNCT_2:5;
S₁[a * b,y] by G1;
then consider a1, b1 being Element of K such that
F4: ( a * b = a1 * b1 & a1 in BE & b1 in BK & a * b in Base (BE,BK) & ex l3 being Linear_Combination of BE st
( Sum l3 = l1 . b1 & y = l3 . a1 ) ) by F3;
consider l3 being Linear_Combination of BE such that
F5: ( Sum l3 = l1 . b1 & y = l3 . a1 ) by F4;
F7: b1 = b by BE0, F4, F3, F1;
then F8: l2 = l3 by F5, F2, ZMODUL033;
H2: 0. (VecSp (K,E)) = 0. K by FIELD_4:def 6;
reconsider b1V = b1 as Element of (VecSp (K,E)) by FIELD_4:def 6;
{b1} c= BK by F4, TARSKI:def 1;
then {b1V} is linearly-independent by VECTSP_7:1;
then F9: b1 <> 0. K by H2, VECTSP_7:3;
b1 * a1 = a1 * b1 by GROUP_1:def 12
.= b1 * a by F4, F7, GROUP_1:def 12 ;
hence l . (a * b) = l2 . a by F8, F5, F9, VECTSP_1:5; :: thesis: verum

end;

hence ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
l . (a * b) = l2 . a ) ) by F2; :: thesis: verum

end;

hence for b being Element of K st b in BK holds
ex l2 being Linear_Combination of BE st
( Sum l2 = l1 . b & ( for a being Element of K st a in BE & a * b in Base (BE,BK) holds
l . (a * b) = l2 . a ) ) ; :: thesis: verum