let F be Field; :: thesis:
let E be FieldExtension of F; :: thesis:
let K be F -extending FieldExtension of F; :: thesis:
let BE be non empty linearly-independent Subset of (VecSp (E,F)); :: thesis:
let BK be non empty linearly-independent Subset of (VecSp (K,E)); :: thesis:
defpred S₁[ object , object ] means ex a, b being Element of K st
( a in BE & b in BK & $1 = a * b & $2 = [a,b] );

let x be object ; :: thesis:
assume x in Base (BE,BK) ; :: thesis:
then consider a, b being Element of K such that
B1: ( x = a * b & a in BE & b in BK ) ;
thus ex y being object st
( y in [:BE,BK:] & S₁[x,y] ) :: thesis:

take [a,b] ; :: thesis:
thus ( [a,b] in [:BE,BK:] & S₁[x,[a,b]] ) by B1, ZFMISC_1:def 2; :: thesis:

end;

let o be object ; :: thesis:
assume o in [:BE,BK:] ; :: thesis:
then consider a, b being object such that
E1: ( a in BE & b in BK & o = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of K by E1, H1, H5;
E0: a * b in Base (BE,BK) by E1;
a * b in dom f by E1, C;
then E2: f . (a * b) in rng f by FUNCT_1:3;
consider a1, b1 being Element of K such that
E3: ( a1 in BE & b1 in BK & a * b = a1 * b1 & f . (a * b) = [a1,b1] ) by E0, B;
E4: b1 = b by BE0, E3, E1;
reconsider bV = b as Element of (VecSp (K,E)) by FIELD_4:def 6;
{b} c= BK by E1, TARSKI:def 1;
then {bV} is linearly-independent by VECTSP_7:1;
then E5: b <> 0. K by H2, VECTSP_7:3;
b * a = a1 * b by E3, E4, GROUP_1:def 12
.= b * a1 by GROUP_1:def 12 ;
hence o in rng f by E1, E2, E3, E4, E5, VECTSP_1:5; :: thesis:

end;

rng f c= [:BE,BK:] ;
hence rng f = [:BE,BK:] by D1, TARSKI:2; :: thesis:

end;

let x1, x2 be object ; :: thesis:
assume F0: ( x1 in Base (BE,BK) & x2 in Base (BE,BK) & f . x1 = f . x2 ) ; :: thesis:
then consider a1, b1 being Element of K such that
F1: ( x1 = a1 * b1 & a1 in BE & b1 in BK ) ;
consider a2, b2 being Element of K such that
F2: ( x2 = a2 * b2 & a2 in BE & b2 in BK ) by F0;
F3: f . (a1 * b1) = [a1,b1]

S₁[a1 * b1,f . (a1 * b1)] by F0, F1, B;
then consider a3, b3 being Element of K such that
E3: ( a3 in BE & b3 in BK & a1 * b1 = a3 * b3 & f . (a3 * b3) = [a3,b3] ) ;
E4: b3 = b1 by BE0, F1, E3;
reconsider b1V = b1 as Element of (VecSp (K,E)) by FIELD_4:def 6;
{b1} c= BK by F1, TARSKI:def 1;
then {b1V} is linearly-independent by VECTSP_7:1;
then E5: b1 <> 0. K by H2, VECTSP_7:3;
b1 * a1 = a3 * b1 by E3, E4, GROUP_1:def 12
.= b1 * a3 by GROUP_1:def 12 ;
hence f . (a1 * b1) = [a1,b1] by E4, E3, E5, VECTSP_1:5; :: thesis:

end;

f . (a2 * b2) = [a2,b2]

S₁[a2 * b2,f . (a2 * b2)] by F0, F2, B;
then consider a3, b3 being Element of K such that
E3: ( a3 in BE & b3 in BK & a2 * b2 = a3 * b3 & f . (a3 * b3) = [a3,b3] ) ;
E4: b3 = b2 by BE0, F2, E3;
reconsider b2V = b2 as Element of (VecSp (K,E)) by FIELD_4:def 6;
{b2} c= BK by F2, TARSKI:def 1;
then {b2V} is linearly-independent by VECTSP_7:1;
then E5: b2 <> 0. K by H2, VECTSP_7:3;
b2 * a2 = a3 * b2 by E3, E4, GROUP_1:def 12
.= b2 * a3 by GROUP_1:def 12 ;
hence f . (a2 * b2) = [a2,b2] by E4, E3, E5, VECTSP_1:5; :: thesis:

end;

end;

end;