for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for BE being non empty linearly-independent Subset of (VecSp (E,F))
for BK being non empty linearly-independent Subset of (VecSp (K,E)) holds card (Base (BE,BK)) = card [:BE,BK:]