deffunc H₁( object ) -> Element of NAT = 0 ;
let p, q be bag of SetPrimes ; :: thesis: ( support p c= support q & p | (support p) = q | (support p) implies ex r being bag of SetPrimes st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q ) )
assume that
A1: support p c= support q and
A2: p | (support p) = q | (support p) ; :: thesis: ex r being bag of SetPrimes st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q )
deffunc H₂( object ) -> set = q . $1;
defpred S₁[ object ] means $1 in (support q) \ (support p);
A3: for x being object st x in SetPrimes holds
( ( S₁[x] implies H₂(x) in NAT ) & ( not S₁[x] implies H₁(x) in NAT ) ) by ORDINAL1:def 12;
consider f being Function of SetPrimes,NAT such that
A4: for x being object 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(A3);
A5: 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 that
x in SetPrimes and
A6: x in (support q) \ (support p) ; :: thesis: f . x <> 0
x in support q by A6, XBOOLE_0:def 5;
then q . x <> 0 by PRE_POLY:def 7;
hence f . x <> 0 by A4, A6; :: thesis: verum

end;

A7: for x being object st not x in SetPrimes holds
f . x = 0

proof

let x be object ; :: 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 2; :: thesis: verum

end;

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

proof

let x be object ; :: 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 A4, A5; :: 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 A7; :: thesis: verum

end;

end;

end;

then support f is finite by PRE_POLY:def 7;
then reconsider r = f as bag of SetPrimes by PRE_POLY:def 8;
A9: (support p) \/ (support r) = (support p) \/ ((support q) \ (support p)) by A8, PRE_POLY:def 7
.= (support p) \/ (support q) by XBOOLE_1:39
.= support q by A1, XBOOLE_1:12 ;
A10: dom (f | (support f)) = (dom f) /\ (support f) by RELAT_1:61
.= support f by PRE_POLY:37, XBOOLE_1:28 ;
A11: support f = (support q) \ (support p) by A8, PRE_POLY:def 7;
A12: for x being object st x in dom (f | (support f)) holds
(f | (support f)) . x = (q | (support f)) . x

proof

let x be object ; :: thesis: ( x in dom (f | (support f)) implies (f | (support f)) . x = (q | (support f)) . x )
assume A13: x in dom (f | (support f)) ; :: thesis: (f | (support f)) . x = (q | (support f)) . x
then A14: (q | (support f)) . x = q . x by A10, FUNCT_1:49;
(f | (support f)) . x = f . x by A10, A13, FUNCT_1:49;
hence (f | (support f)) . x = (q | (support f)) . x by A4, A11, A10, A13, A14; :: thesis: verum

end;

dom (q | (support f)) = (dom q) /\ (support f) by RELAT_1:61
.= (dom q) /\ ((support q) \ (support p)) by A8, PRE_POLY:def 7
.= ((dom q) /\ (support q)) \ (support p) by XBOOLE_1:49
.= (support q) \ (support p) by PRE_POLY:37, XBOOLE_1:28
.= support f by A8, PRE_POLY:def 7 ;
then A15: f | (support f) = q | (support f) by A10, A12, FUNCT_1:def 11;
A16: support p misses support f

proof

assume support p meets support f ; :: thesis: contradiction
then ex x being object st
( x in support p & x in support f ) by XBOOLE_0:3;
hence contradiction by A11, XBOOLE_0:def 5; :: thesis: verum

end;

then (support p) /\ (support f) = {} by XBOOLE_0:def 7;
then p + r = q by A2, A15, A9, Th2;
hence ex r being bag of SetPrimes st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q ) by A11, A16, A15; :: thesis: verum