let R be domRing; :: thesis: 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)
let S1, S2 be non empty finite Subset of R; :: thesis: 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)
let p be Ppoly of R,S1; :: thesis: for q being Ppoly of R,S2 st S1 /\ S2 = {} holds
p *' q is Ppoly of R,(S1 \/ S2)
let q be Ppoly of R,S2; :: thesis: ( S1 /\ S2 = {} implies p *' q is Ppoly of R,(S1 \/ S2) )
assume A: S1 /\ S2 = {} ; :: thesis: p *' q is Ppoly of R,(S1 \/ S2)
reconsider B1 = Bag S1, B2 = Bag S2 as non zero bag of the carrier of R ;
B: ( B1 = (S1,1) -bag & B2 = (S2,1) -bag ) by RING_5:def 1;
S1 misses S2 by A;
then B1 + B2 = ((S1 \/ S2),1) -bag by B, UPROOTS:10
.= Bag (S1 \/ S2) by RING_5:def 1 ;
hence p *' q is Ppoly of R,(S1 \/ S2) by RING_5:58; :: thesis: verum