let F be Field; :: thesis: for E being FieldExtension of F
for K being F -extending FieldExtension of F
for BE being Basis of (VecSp (E,F))
for l1 being Linear_Combination of VecSp (K,E)
for b being Element of K ex l2 being Linear_Combination of BE st l1 . b = Sum l2
let E be FieldExtension of F; :: thesis: for K being F -extending FieldExtension of F
for BE being Basis of (VecSp (E,F))
for l1 being Linear_Combination of VecSp (K,E)
for b being Element of K ex l2 being Linear_Combination of BE st l1 . b = Sum l2
let K be F -extending FieldExtension of F; :: thesis: for BE being Basis of (VecSp (E,F))
for l1 being Linear_Combination of VecSp (K,E)
for b being Element of K ex l2 being Linear_Combination of BE st l1 . b = Sum l2
let BE be Basis of (VecSp (E,F)); :: thesis: for l1 being Linear_Combination of VecSp (K,E)
for b being Element of K ex l2 being Linear_Combination of BE st l1 . b = Sum l2
let l1 be Linear_Combination of VecSp (K,E); :: thesis: for b being Element of K ex l2 being Linear_Combination of BE st l1 . b = Sum l2
let b be Element of K; :: thesis: ex l2 being Linear_Combination of BE st l1 . b = Sum l2
A: the carrier of (VecSp (K,E)) = the carrier of K by FIELD_4:def 6;
B: the carrier of (VecSp (E,F)) = the carrier of E by FIELD_4:def 6;
VecSp (E,F) = Lin BE by VECTSP_7:def 3;
then l1 . b in Lin BE by A, B, FUNCT_2:5;
hence ex l2 being Linear_Combination of BE st l1 . b = Sum l2 by VECTSP_7:7; :: thesis: verum