let E be F -finite FieldExtension of F; :: thesis: E is finite
set V = VecSp (E,F);
set d = dim (VecSp (E,F));
reconsider V = VecSp (E,F) as finite-dimensional VectSp of F by FIELD_4:def 8;
consider T being linear-transformation of V,(F ^* (dim (VecSp (E,F)))) such that
H: T is bijective by VECTSP13:30, VECTSP13:def 10;
( dom T = the carrier of V & rng T = the carrier of (F ^* (dim (VecSp (E,F)))) ) by H, FUNCT_2:def 1, FUNCT_2:def 3;
then A: card the carrier of V = card the carrier of (F ^* (dim (VecSp (E,F)))) by H, CARD_1:70;
the carrier of V = the carrier of E by FIELD_4:def 6;
hence E is finite by A; :: thesis: verum