for F being Field
for p, q being Polynomial of F st p splits_in F & q splits_in F holds
p *' q splits_in F