theorem degmult: :: FIELD_7:30

for F being Field
for E being b₁ -finite FieldExtension of F
for K being b₁ -extending b₂ -finite FieldExtension of F holds deg (K,F) = (deg (K,E)) * (deg (E,F))