let F be Field; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being Subset of (VecSp (K,E))
for BF being Subset of (VecSp (K,F)) st BF c= BE holds
for l being Linear_Combination of BF holds l is Linear_Combination of BE
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F
for BE being Subset of (VecSp (K,E))
for BF being Subset of (VecSp (K,F)) st BF c= BE holds
for l being Linear_Combination of BF holds l is Linear_Combination of BE
let K be E -extending FieldExtension of F; :: thesis: for BE being Subset of (VecSp (K,E))
for BF being Subset of (VecSp (K,F)) st BF c= BE holds
for l being Linear_Combination of BF holds l is Linear_Combination of BE
let BE be Subset of (VecSp (K,E)); :: thesis: for BF being Subset of (VecSp (K,F)) st BF c= BE holds
for l being Linear_Combination of BF holds l is Linear_Combination of BE
let BF be Subset of (VecSp (K,F)); :: thesis: ( BF c= BE implies for l being Linear_Combination of BF holds l is Linear_Combination of BE )
assume AS: BF c= BE ; :: thesis: for l being Linear_Combination of BF holds l is Linear_Combination of BE
let l be Linear_Combination of BF; :: thesis: l is Linear_Combination of BE
reconsider l1 = l as Linear_Combination of VecSp (K,E) by sp0;
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;

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 o in Carrier l1 ; :: thesis: o in BE
then consider v1 being Element of (VecSp (K,E)) such that
A: ( o = v1 & l1 . v1 <> 0. E ) by VECTSP_6:1;
reconsider v = v1 as Element of (VecSp (K,F)) by H0;
0. E = 0. F by H1, C0SP1:def 3;
then B: v in Carrier l by A, VECTSP_6:1;
Carrier l c= BF by VECTSP_6:def 4;
hence o in BE by B, A, AS; :: thesis: verum

end;

then Carrier l1 c= BE ;
hence l is Linear_Combination of BE by VECTSP_6:def 4; :: thesis: verum