let F1, F2 be Field; :: thesis: for p being Polynomial of F1 st F1 == F2 holds
p is Polynomial of F2
let p be Polynomial of F1; :: thesis: ( F1 == F2 implies p is Polynomial of F2 )
assume F1 == F2 ; :: thesis: p is Polynomial of F2
then F1 is Subfield of F2 by FIELD_7:def 2;
then F1 is Subring of F2 by FIELD_5:12;
hence p is Polynomial of F2 by FIELD_4:9; :: thesis: verum