let F be Field; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F st K is F -finite holds
( E is F -finite & deg (E,F) <= deg (K,F) & K is E -finite & deg (K,E) <= deg (K,F) )
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F st K is F -finite holds
( E is F -finite & deg (E,F) <= deg (K,F) & K is E -finite & deg (K,E) <= deg (K,F) )
let K be E -extending FieldExtension of F; :: thesis: ( K is F -finite implies ( E is F -finite & deg (E,F) <= deg (K,F) & K is E -finite & deg (K,E) <= deg (K,F) ) )
assume AS: K is F -finite ; :: thesis: ( E is F -finite & deg (E,F) <= deg (K,F) & K is E -finite & deg (K,E) <= deg (K,F) )
hence ( E is F -finite & deg (E,F) <= deg (K,F) ) by FIELD_5:15; :: thesis: ( K is E -finite & deg (K,E) <= deg (K,F) )
set BF = the Basis of (VecSp (K,F));
reconsider BF = the Basis of (VecSp (K,F)) as finite Subset of (VecSp (K,F)) by AS;
H0: the carrier of (VecSp (K,E)) = the carrier of K by FIELD_4:def 6
.= the carrier of (VecSp (K,F)) by FIELD_4:def 6 ;
then reconsider BE = BF as finite Subset of (VecSp (K,E)) ;
Lin BE = VecSp (K,E)

proof

H1: the carrier of (Lin BE) c= the carrier of (VecSp (K,E)) by VECTSP_4:def 2;
the carrier of (VecSp (K,E)) c= the carrier of (Lin BE)

proof

now :: thesis: for o being object st o in the carrier of (VecSp (K,E)) holds
o in the carrier of (Lin BE)

let o be object ; :: thesis: ( o in the carrier of (VecSp (K,E)) implies o in the carrier of (Lin BE) )
assume o in the carrier of (VecSp (K,E)) ; :: thesis: o in the carrier of (Lin BE)
then o in Lin BF by H0, VECTSP_7:def 3;
then consider l being Linear_Combination of BF such that
H2: o = Sum l by VECTSP_7:7;
reconsider l1 = l as Linear_Combination of BE by sp1;
o = Sum l1 by H2, sp2;
then o in Lin BE by VECTSP_7:7;
hence o in the carrier of (Lin BE) ; :: thesis: verum

end;

hence the carrier of (VecSp (K,E)) c= the carrier of (Lin BE) ; :: thesis: verum

end;

hence Lin BE = VecSp (K,E) by H1, TARSKI:2, VECTSP_4:31; :: thesis: verum

end;

then consider I being Subset of (VecSp (K,E)) such that
A: ( I c= BE & I is linearly-independent & Lin I = VecSp (K,E) ) by VECTSP_7:18;
reconsider I = I as finite Subset of (VecSp (K,E)) by A;
B: I is Basis of (VecSp (K,E)) by A, VECTSP_7:def 3;
D: VecSp (K,E) is finite-dimensional by A, VECTSP_7:def 3, MATRLIN:def 1;
hence K is E -finite by FIELD_4:def 8; :: thesis: deg (K,E) <= deg (K,F)
VecSp (K,F) is finite-dimensional by AS, FIELD_4:def 8;
then F: ( dim (VecSp (K,E)) = card I & dim (VecSp (K,F)) = card BE ) by B, D, VECTSP_9:def 1;
( deg (K,E) = dim (VecSp (K,E)) & deg (K,F) = dim (VecSp (K,F)) ) by AS, D, FIELD_4:def 7;
hence deg (K,E) <= deg (K,F) by F, A, NAT_1:43; :: thesis: verum