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