let F1, F2 be Field; :: thesis: for p being non zero Polynomial of F1 st F1 == F2 holds
p is non zero Polynomial of F2
let p be non zero Polynomial of F1; :: thesis: ( F1 == F2 implies p is non zero Polynomial of F2 )
assume AS: F1 == F2 ; :: thesis: p is non zero Polynomial of F2
then reconsider p1 = p as Polynomial of F2 by lift6a;

now :: thesis: not p1 is zero

assume p1 is zero ; :: thesis: contradiction
then p1 = 0_. F2 by UPROOTS:def 5
.= 0_. F1 by AS, lift6b ;
hence contradiction ; :: thesis: verum

end;

hence p is non zero Polynomial of F2 ; :: thesis: verum