let F be Field; :: thesis: for E1 being FieldExtension of F
for E2 being Field st E1 == E2 holds
E2 is FieldExtension of F
let E1 be FieldExtension of F; :: thesis: for E2 being Field st E1 == E2 holds
E2 is FieldExtension of F
let E2 be Field; :: thesis: ( E1 == E2 implies E2 is FieldExtension of F )
assume E1 == E2 ; :: thesis: E2 is FieldExtension of F
then A: E1 is Subfield of E2 by FIELD_7:def 2;
F is Subfield of E1 by FIELD_4:7;
then F is Subfield of E2 by A, EC_PF_1:5;
hence E2 is FieldExtension of F by FIELD_4:7; :: thesis: verum