theorem r58: :: FIELD_14:28

for R being domRing
for S1, S2 being non empty finite Subset of R
for p being Ppoly of R,S1
for q being Ppoly of R,S2 st S1 /\ S2 = {} holds
p *' q is Ppoly of R,(S1 \/ S2)