let F be Field; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for l being Linear_Combination of VecSp (K,F) holds l is Linear_Combination of VecSp (K,E)
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F
for l being Linear_Combination of VecSp (K,F) holds l is Linear_Combination of VecSp (K,E)
let K be E -extending FieldExtension of F; :: thesis: for l being Linear_Combination of VecSp (K,F) holds l is Linear_Combination of VecSp (K,E)
let l be Linear_Combination of VecSp (K,F); :: thesis: l is Linear_Combination of VecSp (K,E)
H0: the carrier of (VecSp (K,F)) = the carrier of K by FIELD_4:def 6
.= the carrier of (VecSp (K,E)) by FIELD_4:def 6 ;
H1: ( F is Subring of E & E is Subring of K ) by FIELD_4:def 1;
then H2: ( the carrier of F c= the carrier of E & the carrier of E c= the carrier of K ) by C0SP1:def 3;
rng l c= the carrier of E by H2;
then l is Function of the carrier of (VecSp (K,E)), the carrier of E by H0, FUNCT_2:6;
then A: l in Funcs ( the carrier of (VecSp (K,E)), the carrier of E) by FUNCT_2:8;
consider T being finite Subset of (VecSp (K,F)) such that
B: for v being Element of (VecSp (K,F)) st not v in T holds
l . v = 0. F by VECTSP_6:def 1;
reconsider T1 = T as finite Subset of (VecSp (K,E)) by H0;

now :: thesis: for v1 being Element of (VecSp (K,E)) st not v1 in T1 holds
l . v1 = 0. E

let v1 be Element of (VecSp (K,E)); :: thesis: ( not v1 in T1 implies l . v1 = 0. E )
assume C: not v1 in T1 ; :: thesis: l . v1 = 0. E
reconsider v = v1 as Element of (VecSp (K,F)) by H0;
l . v = 0. F by B, C;
hence l . v1 = 0. E by H1, C0SP1:def 3; :: thesis: verum

end;

hence l is Linear_Combination of VecSp (K,E) by A, VECTSP_6:def 1; :: thesis: verum