let p, q be bag of ; :: thesis: ( support p c= support q & p | (support p) = q | (support p) implies ex r being bag of st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q ) )
assume A1: ( support p c= support q & p | (support p) = q | (support p) ) ; :: thesis: ex r being bag of st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q )
defpred S₁[ set ] means $1 in (support q) \ (support p);
deffunc H₁( set ) -> Element of NAT = q . $1;
deffunc H₂( set ) -> Element of NAT = 0 ;
A2: for x being set st x in SetPrimes holds
( ( S₁[x] implies H₁(x) in NAT ) & ( not S₁[x] implies H₂(x) in NAT ) ) ;
consider f being Function of SetPrimes ,NAT such that
A3: for x being set st x in SetPrimes holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) from FUNCT_2:sch 5(A2);
A4: for x being set st x in SetPrimes & x in (support q) \ (support p) holds
f . x <> 0

proof

let x be set ; :: thesis: ( x in SetPrimes & x in (support q) \ (support p) implies f . x <> 0 )
assume A5: ( x in SetPrimes & x in (support q) \ (support p) ) ; :: thesis: f . x <> 0
then x in support q by XBOOLE_0:def 5;
then q . x <> 0 by POLYNOM1:def 7;
hence f . x <> 0 by A3, A5; :: thesis: verum

end;

A6: for x being set st not x in SetPrimes holds
f . x = 0

proof

let x be set ; :: thesis: ( not x in SetPrimes implies f . x = 0 )
assume not x in SetPrimes ; :: thesis: f . x = 0
then not x in dom f ;
hence f . x = 0 by FUNCT_1:def 4; :: thesis: verum

end;

A7: for x being set holds
( x in (support q) \ (support p) iff f . x <> 0 )

proof

let x be set ; :: thesis: ( x in (support q) \ (support p) iff f . x <> 0 )

per cases ( x in SetPrimes or not x in SetPrimes ) ;

suppose x in SetPrimes ; :: thesis: ( x in (support q) \ (support p) iff f . x <> 0 )

hence ( x in (support q) \ (support p) iff f . x <> 0 ) by A3, A4; :: thesis: verum

end;

suppose not x in SetPrimes ; :: thesis: ( x in (support q) \ (support p) iff f . x <> 0 )

hence ( x in (support q) \ (support p) iff f . x <> 0 ) by A6; :: thesis: verum

end;

end;

end;

A8: support f = (support q) \ (support p) by A7, POLYNOM1:def 7;
A9: support p misses support f

proof

assume support p meets support f ; :: thesis: contradiction
then consider x being set such that
A10: ( x in support p & x in support f ) by XBOOLE_0:3;
thus contradiction by A8, A10, XBOOLE_0:def 5; :: thesis: verum

end;

then A11: (support p) /\ (support f) = {} by XBOOLE_0:def 7;
A12: f | (support f) = q | (support f)

proof

A13: dom (f | (support f)) = (dom f) /\ (support f) by RELAT_1:90
.= support f by POLYNOM1:41, XBOOLE_1:28 ;
A14: dom (q | (support f)) = (dom q) /\ (support f) by RELAT_1:90
.= (dom q) /\ ((support q) \ (support p)) by A7, POLYNOM1:def 7
.= ((dom q) /\ (support q)) \ (support p) by XBOOLE_1:49
.= (support q) \ (support p) by POLYNOM1:41, XBOOLE_1:28
.= support f by A7, POLYNOM1:def 7 ;
for x being set st x in dom (f | (support f)) holds
(f | (support f)) . x = (q | (support f)) . x

proof

let x be set ; :: thesis: ( x in dom (f | (support f)) implies (f | (support f)) . x = (q | (support f)) . x )
assume A15: x in dom (f | (support f)) ; :: thesis: (f | (support f)) . x = (q | (support f)) . x
then ( (f | (support f)) . x = f . x & (q | (support f)) . x = q . x ) by A13, FUNCT_1:72;
hence (f | (support f)) . x = (q | (support f)) . x by A3, A8, A13, A15; :: thesis: verum

end;

hence f | (support f) = q | (support f) by A13, A14, FUNCT_1:def 17; :: thesis: verum

end;

A16: support f is finite by A7, POLYNOM1:def 7;
reconsider r = f as bag of by A16, POLYNOM1:def 8;
(support p) \/ (support r) = (support p) \/ ((support q) \ (support p)) by A7, POLYNOM1:def 7
.= (support p) \/ (support q) by XBOOLE_1:39
.= support q by A1, XBOOLE_1:12 ;
then p + r = q by A1, A11, A12, Th2;
hence ex r being bag of st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q ) by A8, A9, A12; :: thesis: verum