let F be Field; :: thesis: for E being FieldExtension of F

for K being b_{1} -extending FieldExtension of F holds

( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )

let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F holds

( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )

let K be E -extending FieldExtension of F; :: thesis: ( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )

set VK = VecSp (K,F);

set VE = VecSp (E,F);

for K being b

( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )

let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F holds

( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )

let K be E -extending FieldExtension of F; :: thesis: ( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )

set VK = VecSp (K,F);

set VE = VecSp (E,F);

now :: thesis: ( K is F -finite implies ( E is F -finite & deg (E,F) <= deg (K,F) ) )

hence
( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )
; :: thesis: verumassume
K is F -finite
; :: thesis: ( E is F -finite & deg (E,F) <= deg (K,F) )

then reconsider VK = VecSp (K,F) as finite-dimensional VectSp of F by FIELD_4:def 8;

A: deg (K,F) = dim VK by FIELD_4:def 7;

B: VecSp (E,F) is Subspace of VK by sp;

then C: dim (VecSp (E,F)) <= dim VK by VECTSP_9:25;

thus E is F -finite by B, FIELD_4:def 8; :: thesis: deg (E,F) <= deg (K,F)

thus deg (E,F) <= deg (K,F) by A, C, FIELD_4:def 7; :: thesis: verum

end;then reconsider VK = VecSp (K,F) as finite-dimensional VectSp of F by FIELD_4:def 8;

A: deg (K,F) = dim VK by FIELD_4:def 7;

B: VecSp (E,F) is Subspace of VK by sp;

then C: dim (VecSp (E,F)) <= dim VK by VECTSP_9:25;

thus E is F -finite by B, FIELD_4:def 8; :: thesis: deg (E,F) <= deg (K,F)

thus deg (E,F) <= deg (K,F) by A, C, FIELD_4:def 7; :: thesis: verum