let F be Field; :: thesis: for E being FieldExtension of F holds
( deg (E,F) = 1 iff E == F )
let E be FieldExtension of F; :: thesis: ( deg (E,F) = 1 iff E == F )

now :: thesis: ( deg (E,F) = 1 implies E == F )

assume deg (E,F) = 1 ; :: thesis: E == F
then A: the carrier of E = the carrier of F by quah1;
F is Subfield of E by FIELD_4:7;
then ( the carrier of F c= the carrier of E & the addF of F = the addF of E || the carrier of F & the multF of F = the multF of E || the carrier of F & 1. F = 1. E & 0. F = 0. E ) by EC_PF_1:def 1;
hence E == F by A; :: thesis: verum

end;

hence ( deg (E,F) = 1 iff E == F ) by quah1; :: thesis: verum