theorem BasKEF: :: FIELD_7:29

for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending b₂ -finite FieldExtension of F
for BE being Basis of (VecSp (E,F))
for BK being Basis of (VecSp (K,E)) holds Base (BE,BK) is Basis of (VecSp (K,F))