theorem F811: :: FIELD_13:7

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