for F being Field
for E being FieldExtension of F
for a being non zero Element of F
for b being non zero Element of E
for p being Ppoly of F
for q being Ppoly of E st a * p = b * q holds
( a = b & p = q )