let F1, F2 be Field; :: thesis: for p being Ppoly of F1 st F1 == F2 holds
p is Ppoly of F2
let p be Ppoly of F1; :: thesis: ( F1 == F2 implies p is Ppoly of F2 )
assume F1 == F2 ; :: thesis: p is Ppoly of F2
then F1 is Subfield of F2 by FIELD_7:def 2;
then F2 is FieldExtension of F1 by FIELD_4:7;
hence p is Ppoly of F2 by FIELD_8:24; :: thesis: verum