let F be Field; :: thesis: for E being F -finite FieldExtension of F
for K being F -extending b₁ -finite FieldExtension of F holds deg (K,F) = (deg (K,E)) * (deg (E,F))
let E be F -finite FieldExtension of F; :: thesis: for K being F -extending E -finite FieldExtension of F holds deg (K,F) = (deg (K,E)) * (deg (E,F))
let K be F -extending E -finite FieldExtension of F; :: thesis: deg (K,F) = (deg (K,E)) * (deg (E,F))
set BE = the Basis of (VecSp (E,F));
set BK = the Basis of (VecSp (K,E));
the Basis of (VecSp (E,F)) is finite ;
then B1: VecSp (E,F) is finite-dimensional by MATRLIN:def 1;
the Basis of (VecSp (K,E)) is finite ;
then B2: VecSp (K,E) is finite-dimensional by MATRLIN:def 1;
A: Base ( the Basis of (VecSp (E,F)), the Basis of (VecSp (K,E))) is Basis of (VecSp (K,F)) by BasKEF;
then B: VecSp (K,F) is finite-dimensional by MATRLIN:def 1;
hence deg (K,F) = dim (VecSp (K,F)) by FIELD_4:def 7
.= card (Base ( the Basis of (VecSp (E,F)), the Basis of (VecSp (K,E)))) by VECTSP_9:def 1, B, A
.= (card the Basis of (VecSp (E,F))) * (card the Basis of (VecSp (K,E))) by BE2
.= (dim (VecSp (E,F))) * (card the Basis of (VecSp (K,E))) by VECTSP_9:def 1, B1
.= (deg (E,F)) * (card the Basis of (VecSp (K,E))) by FIELD_4:def 7
.= (deg (E,F)) * (dim (VecSp (K,E))) by VECTSP_9:def 1, B2
.= (deg (K,E)) * (deg (E,F)) by FIELD_4:def 7 ;
:: thesis: verum