theorem T2: :: FIELD_7:28

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 Lin (Base (BE,BK)) = ModuleStr(# the carrier of (VecSp (K,F)), the addF of (VecSp (K,F)), the ZeroF of (VecSp (K,F)), the lmult of (VecSp (K,F)) #)