for F being Field
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