let F be Field; 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; 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; 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)); 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); for b being Element of K ex l2 being Linear_Combination of BE st l1 . b = Sum l2
let b be Element of K; 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; verum