let F be Field; for E being FieldExtension of F
for K being b1 -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; 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; ( 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 ( K is F -finite implies ( E is F -finite & deg (E,F) <= deg (K,F) ) )assume
K is
F -finite
;
( 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;
deg (E,F) <= deg (K,F)thus
deg (
E,
F)
<= deg (
K,
F)
by A, C, FIELD_4:def 7;
verum end;
hence
( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )
; verum