let F be Field; :: thesis: for E being F -finite FieldExtension of F
for a being Element of E holds deg (a,F) divides deg (E,F)
let E be F -finite FieldExtension of F; :: thesis: for a being Element of E holds deg (a,F) divides deg (E,F)
let a be Element of E; :: thesis: deg (a,F) divides deg (E,F)
set K = FAdj (F,{a});
reconsider E1 = E as F -extending FAdj (F,{a}) -finite FieldExtension of F by FIELD_4:7, FIELD_7:31;
deg (E1,F) = (deg (E1,(FAdj (F,{a})))) * (deg (a,F)) by FIELD_7:30;
hence deg (a,F) divides deg (E,F) by INT_1:def 3; :: thesis: verum