theorem T2:
for
F being
Field for
E being
b1 -finite FieldExtension of
F for
K being
b1 -extending b2 -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)) #)