let F be Field; :: thesis: for E1, E2 being FieldExtension of F st E1 == E2 holds
deg (E1,F) = deg (E2,F)
let E1, E2 be FieldExtension of F; :: thesis: ( E1 == E2 implies deg (E1,F) = deg (E2,F) )
set V1 = VecSp (E1,F);
set V2 = VecSp (E2,F);
assume E1 == E2 ; :: thesis: deg (E1,F) = deg (E2,F)
then AS: VecSp (E1,F) = VecSp (E2,F) by str12;

per cases ( VecSp (E1,F) is finite-dimensional or not VecSp (E1,F) is finite-dimensional ) ;

suppose F: VecSp (E1,F) is finite-dimensional ; :: thesis: deg (E1,F) = deg (E2,F)

hence deg (E1,F) = dim (VecSp (E2,F)) by AS, FIELD_4:def 7
.= deg (E2,F) by AS, F, FIELD_4:def 7 ;
:: thesis: verum

end;

suppose F: not VecSp (E1,F) is finite-dimensional ; :: thesis: deg (E1,F) = deg (E2,F)

hence deg (E1,F) = - 1 by FIELD_4:def 7
.= deg (E2,F) by AS, F, FIELD_4:def 7 ;
:: thesis: verum

end;

end;