let p be bag of SetPrimes ; :: thesis: for X being set st X c= support p holds
ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p )
let X be set ; :: thesis: ( X c= support p implies ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p ) )
set fq = p +* (X --> 0);
A1: rng (p +* (X --> 0)) c= (rng p) \/ (rng (X --> 0)) by FUNCT_4:17;
A2: rng (X --> 0) c= NAT by RELAT_1:def 19;
A3: rng p c= NAT by VALUED_0:def 6;
then (rng p) \/ (rng (X --> 0)) c= NAT by A2, XBOOLE_1:8;
then A4: rng (p +* (X --> 0)) c= NAT by A1, XBOOLE_1:1;
set fr = p +* ((SetPrimes \ X) --> 0);
A5: dom (p +* ((SetPrimes \ X) --> 0)) = (dom p) \/ (dom ((SetPrimes \ X) --> 0)) by FUNCT_4:def 1
.= (dom p) \/ (SetPrimes \ X) by FUNCOP_1:13
.= SetPrimes \/ (SetPrimes \ X) by PARTFUN1:def 2
.= SetPrimes by XBOOLE_1:12, XBOOLE_1:36 ;
A6: rng (p +* ((SetPrimes \ X) --> 0)) c= (rng p) \/ (rng ((SetPrimes \ X) --> 0)) by FUNCT_4:17;
rng ((SetPrimes \ X) --> 0) c= NAT by RELAT_1:def 19;
then (rng p) \/ (rng ((SetPrimes \ X) --> 0)) c= NAT by A3, XBOOLE_1:8;
then rng (p +* ((SetPrimes \ X) --> 0)) c= NAT by A6, XBOOLE_1:1;
then reconsider fr = p +* ((SetPrimes \ X) --> 0) as Function of SetPrimes,NAT by A5, FUNCT_2:def 1, RELSET_1:4;
assume A7: X c= support p ; :: thesis: ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p )
A8: for x being set st not x in X & x in SetPrimes holds
fr . x = 0

proof

let x be set ; :: thesis: ( not x in X & x in SetPrimes implies fr . x = 0 )
assume that
A9: not x in X and
A10: x in SetPrimes ; :: thesis: fr . x = 0
A11: x in SetPrimes \ X by A9, A10, XBOOLE_0:def 5;
then x in dom ((SetPrimes \ X) --> 0) by FUNCOP_1:13;
then fr . x = ((SetPrimes \ X) --> 0) . x by FUNCT_4:13;
hence fr . x = 0 by A11, FUNCOP_1:7; :: thesis: verum

end;

A12: dom (X --> 0) = X by FUNCOP_1:13;
then dom (p +* (X --> 0)) = (dom p) \/ X by FUNCT_4:def 1
.= SetPrimes \/ X by PARTFUN1:def 2
.= SetPrimes by A7, XBOOLE_1:1, XBOOLE_1:12 ;
then reconsider fq = p +* (X --> 0) as Function of SetPrimes,NAT by A4, FUNCT_2:def 1, RELSET_1:4;
A13: dom (fq | (support fq)) = (dom fq) /\ (support fq) by RELAT_1:61
.= support fq by PRE_POLY:37, XBOOLE_1:28 ;
A14: for x being set st not x in SetPrimes holds
( fr . x = 0 & fq . x = 0 )

proof

let x be set ; :: thesis: ( not x in SetPrimes implies ( fr . x = 0 & fq . x = 0 ) )
assume A15: not x in SetPrimes ; :: thesis: ( fr . x = 0 & fq . x = 0 )
then A16: not x in dom fr ;
not x in dom fq by A15;
hence ( fr . x = 0 & fq . x = 0 ) by A16, FUNCT_1:def 2; :: thesis: verum

end;

A17: for x being set st x in X holds
fr . x = p . x

proof

let x be set ; :: thesis: ( x in X implies fr . x = p . x )
assume x in X ; :: thesis: fr . x = p . x
then not x in dom ((SetPrimes \ X) --> 0) by XBOOLE_0:def 5;
hence fr . x = p . x by FUNCT_4:11; :: thesis: verum

end;

A18: for x being set st x in SetPrimes & x in X holds
fr . x <> 0

proof

let x be set ; :: thesis: ( x in SetPrimes & x in X implies fr . x <> 0 )
assume that
x in SetPrimes and
A19: x in X ; :: thesis: fr . x <> 0
p . x <> 0 by A7, A19, PRE_POLY:def 7;
hence fr . x <> 0 by A17, A19; :: thesis: verum

end;

A20: for x being set holds
( x in X iff fr . x <> 0 )

proof

let x be set ; :: thesis: ( x in X iff fr . x <> 0 )

now :: thesis: ( x in X iff fr . x <> 0 )

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

suppose x in SetPrimes ; :: thesis: ( x in X iff fr . x <> 0 )

hence ( x in X iff fr . x <> 0 ) by A8, A18; :: thesis: verum

end;

suppose A21: not x in SetPrimes ; :: thesis: ( x in X iff fr . x <> 0 )

X c= SetPrimes by A7, XBOOLE_1:1;
hence ( x in X iff fr . x <> 0 ) by A14, A21; :: thesis: verum

end;

end;

end;

hence ( x in X iff fr . x <> 0 ) ; :: thesis: verum

end;

then A22: support fr = X by PRE_POLY:def 7;
then reconsider r = fr as bag of SetPrimes by A7, PRE_POLY:def 8;
A23: support p c= dom p by PRE_POLY:37;
A24: dom (fr | (support fr)) = (dom fr) /\ (support fr) by RELAT_1:61
.= support fr by PRE_POLY:37, XBOOLE_1:28
.= X by A20, PRE_POLY:def 7 ;
A25: for x being set st x in dom (fr | (support fr)) holds
(fr | (support fr)) . x = (p | (support fr)) . x

proof

let x be set ; :: thesis: ( x in dom (fr | (support fr)) implies (fr | (support fr)) . x = (p | (support fr)) . x )
assume A26: x in dom (fr | (support fr)) ; :: thesis: (fr | (support fr)) . x = (p | (support fr)) . x
then A27: (p | (support fr)) . x = p . x by A22, A24, FUNCT_1:49;
(fr | (support fr)) . x = fr . x by A22, A24, A26, FUNCT_1:49;
hence (fr | (support fr)) . x = (p | (support fr)) . x by A17, A24, A26, A27; :: thesis: verum

end;

dom (p | (support fr)) = (dom p) /\ (support fr) by RELAT_1:61
.= (dom p) /\ X by A20, PRE_POLY:def 7
.= X by A7, A23, XBOOLE_1:1, XBOOLE_1:28 ;
then A28: fr | (support fr) = p | (support fr) by A24, A25, FUNCT_1:def 11;
A29: for x being set st x in X holds
fq . x = 0

proof

let x be set ; :: thesis: ( x in X implies fq . x = 0 )
assume A30: x in X ; :: thesis: fq . x = 0
hence fq . x = (X --> 0) . x by A12, FUNCT_4:13
.= 0 by A30, FUNCOP_1:7 ;
:: thesis: verum

end;

A31: for x being set holds
( x in (support p) \ X iff fq . x <> 0 )

proof

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

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

suppose x in X ; :: thesis: ( x in (support p) \ X iff fq . x <> 0 )

hence ( x in (support p) \ X iff fq . x <> 0 ) by A29, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A32: not x in X ; :: thesis: ( x in (support p) \ X iff fq . x <> 0 )

then A33: fq . x = p . x by A12, FUNCT_4:11;

per cases ( x in support p or not x in support p ) ;

suppose x in support p ; :: thesis: ( x in (support p) \ X iff fq . x <> 0 )

hence ( x in (support p) \ X iff fq . x <> 0 ) by A32, A33, PRE_POLY:def 7, XBOOLE_0:def 5; :: thesis: verum

end;

suppose not x in support p ; :: thesis: ( x in (support p) \ X iff fq . x <> 0 )

hence ( x in (support p) \ X iff fq . x <> 0 ) by A33, PRE_POLY:def 7, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

end;

end;

then A34: support fq = (support p) \ X by PRE_POLY:def 7;
then reconsider q = fq as bag of SetPrimes by PRE_POLY:def 8;
A35: dom (p | (support fq)) = (dom p) /\ (support fq) by RELAT_1:61
.= (dom p) /\ ((support p) \ X) by A31, PRE_POLY:def 7
.= ((dom p) /\ (support p)) \ X by XBOOLE_1:49
.= (support p) \ X by PRE_POLY:37, XBOOLE_1:28
.= support fq by A31, PRE_POLY:def 7 ;
(support p) \ X misses X by XBOOLE_1:79;
then A36: (support fq) /\ (support fr) = {} by A22, A34, XBOOLE_0:def 7;
A37: for x being set st x in SetPrimes & x in support fq holds
p . x = fq . x

proof

let x be set ; :: thesis: ( x in SetPrimes & x in support fq implies p . x = fq . x )
assume that
x in SetPrimes and
A38: x in support fq ; :: thesis: p . x = fq . x
not x in X by A22, A36, A38, XBOOLE_0:def 4;
hence p . x = fq . x by A12, FUNCT_4:11; :: thesis: verum

end;

for x being set st x in dom (fq | (support fq)) holds
(fq | (support fq)) . x = (p | (support fq)) . x

proof

let x be set ; :: thesis: ( x in dom (fq | (support fq)) implies (fq | (support fq)) . x = (p | (support fq)) . x )
assume A39: x in dom (fq | (support fq)) ; :: thesis: (fq | (support fq)) . x = (p | (support fq)) . x
then A40: (p | (support fq)) . x = p . x by A13, FUNCT_1:49;
(fq | (support fq)) . x = fq . x by A13, A39, FUNCT_1:49;
hence (fq | (support fq)) . x = (p | (support fq)) . x by A13, A37, A39, A40; :: thesis: verum

end;

then A41: fq | (support fq) = p | (support fq) by A13, A35, FUNCT_1:def 11;
(support fr) \/ (support fq) = (support fr) \/ ((support p) \ (support fr)) by A20, A34, PRE_POLY:def 7
.= (support fr) \/ (support p) by XBOOLE_1:39
.= support p by A7, A22, XBOOLE_1:12 ;
then q + r = p by A36, A41, A28, Th2;
hence ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p ) by A22, A34, A41, A28, XBOOLE_1:79; :: thesis: verum