let F be Field; :: thesis: for p, q being Polynomial of F st p splits_in F & q splits_in F holds
p *' q splits_in F
let p, q be Polynomial of F; :: thesis: ( p splits_in F & q splits_in F implies p *' q splits_in F )
assume AS: ( p splits_in F & q splits_in F ) ; :: thesis: p *' q splits_in F
then consider b being non zero Element of F, u being Ppoly of F such that
A: p = b * u by FIELD_4:def 5;
consider c being non zero Element of F, v being Ppoly of F such that
B: q = c * v by AS, FIELD_4:def 5;
D: u *' v is Ppoly of F by RING_5:52;
p *' q = c * ((b * u) *' v) by A, B, RING_4:10
.= c * (b * (u *' v)) by RING_4:10
.= (c * b) * (u *' v) by RING_4:11
.= (b * c) * (u *' v) by GROUP_1:def 12 ;
hence p *' q splits_in F by D, FIELD_4:def 5; :: thesis: verum