for F being Field
for p being non constant Polynomial of F
for q being non zero Polynomial of F st p *' q splits_in F holds
p splits_in F