:: deftheorem defines splits_in FIELD_4:def 5 :
for R being Ring
for S being non degenerated Ring
for p being Polynomial of R holds
( p splits_in S iff ex a being non zero Element of S ex q being Ppoly of S st p = a * q );