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);
A3: rng (p +* (X --> 0)) c= NAT ;
set fr = p +* ((SetPrimes \ X) --> 0);
A4: 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 ;
rng (p +* ((SetPrimes \ X) --> 0)) c= NAT ;
then reconsider fr = p +* ((SetPrimes \ X) --> 0) as Function of SetPrimes,NAT by A4, FUNCT_2:def 1, RELSET_1:4;
assume A6: 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 )
A7: for x being object st not x in X & x in SetPrimes holds
fr . x = 0

proof

let x be object ; :: thesis: ( not x in X & x in SetPrimes implies fr . x = 0 )
assume that
A8: not x in X and
A9: x in SetPrimes ; :: thesis: fr . x = 0
A10: x in SetPrimes \ X by A8, A9, 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 A10, FUNCOP_1:7; :: thesis: verum

end;

A11: 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 A6, XBOOLE_1:1, XBOOLE_1:12 ;
then reconsider fq = p +* (X --> 0) as Function of SetPrimes,NAT by A3, FUNCT_2:def 1, RELSET_1:4;
A12: dom (fq | (support fq)) = (dom fq) /\ (support fq) by RELAT_1:61
.= support fq by PRE_POLY:37, XBOOLE_1:28 ;
A13: for x being object st not x in SetPrimes holds
( fr . x = 0 & fq . x = 0 )

proof

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

end;

A16: for x being object st x in X holds
fr . x = p . x

proof

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

A17: for x being object st x in SetPrimes & x in X holds
fr . x <> 0

proof

let x be object ; :: thesis: ( x in SetPrimes & x in X implies fr . x <> 0 )
assume that
x in SetPrimes and
A18: x in X ; :: thesis: fr . x <> 0
p . x <> 0 by A6, A18, PRE_POLY:def 7;
hence fr . x <> 0 by A16, A18; :: thesis: verum

end;

A19: for x being object holds
( x in X iff fr . x <> 0 )

proof

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

end;

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

X c= SetPrimes by A6, XBOOLE_1:1;
hence ( x in X iff fr . x <> 0 ) by A13, A20; :: thesis: verum

end;

end;

end;

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

end;

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

proof

let x be object ; :: thesis: ( x in dom (fr | (support fr)) implies (fr | (support fr)) . x = (p | (support fr)) . x )
assume A25: x in dom (fr | (support fr)) ; :: thesis: (fr | (support fr)) . x = (p | (support fr)) . x
then A26: (p | (support fr)) . x = p . x by A21, A23, FUNCT_1:49;
(fr | (support fr)) . x = fr . x by A21, A23, A25, FUNCT_1:49;
hence (fr | (support fr)) . x = (p | (support fr)) . x by A16, A23, A25, A26; :: thesis: verum

end;

dom (p | (support fr)) = (dom p) /\ (support fr) by RELAT_1:61
.= (dom p) /\ X by A19, PRE_POLY:def 7
.= X by A6, A22, XBOOLE_1:1, XBOOLE_1:28 ;
then A27: fr | (support fr) = p | (support fr) by A23, A24, FUNCT_1:def 11;
A28: for x being object st x in X holds
fq . x = 0

proof

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

end;

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

proof

let x be object ; :: 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 A28, XBOOLE_0:def 5; :: thesis: verum

end;

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

then A32: fq . x = p . x by A11, 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 A31, A32, 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 A32, PRE_POLY:def 7, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

end;

end;

then A33: support fq = (support p) \ X by PRE_POLY:def 7;
then reconsider q = fq as bag of SetPrimes by PRE_POLY:def 8;
A34: dom (p | (support fq)) = (dom p) /\ (support fq) by RELAT_1:61
.= (dom p) /\ ((support p) \ X) by A30, 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 A30, PRE_POLY:def 7 ;
(support p) \ X misses X by XBOOLE_1:79;
then A35: (support fq) /\ (support fr) = {} by A21, A33, XBOOLE_0:def 7;
A36: 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
A37: x in support fq ; :: thesis: p . x = fq . x
not x in X by A21, A35, A37, XBOOLE_0:def 4;
hence p . x = fq . x by A11, FUNCT_4:11; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in dom (fq | (support fq)) implies (fq | (support fq)) . x = (p | (support fq)) . x )
assume A38: x in dom (fq | (support fq)) ; :: thesis: (fq | (support fq)) . x = (p | (support fq)) . x
then A39: (p | (support fq)) . x = p . x by A12, FUNCT_1:49;
(fq | (support fq)) . x = fq . x by A12, A38, FUNCT_1:49;
hence (fq | (support fq)) . x = (p | (support fq)) . x by A12, A36, A38, A39; :: thesis: verum

end;

then A40: fq | (support fq) = p | (support fq) by A12, A34, FUNCT_1:def 11;
(support fr) \/ (support fq) = (support fr) \/ ((support p) \ (support fr)) by A19, A33, PRE_POLY:def 7
.= (support fr) \/ (support p) by XBOOLE_1:39
.= support p by A6, A21, XBOOLE_1:12 ;
then q + r = p by A35, A40, A27, 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 A21, A33, A40, A27, XBOOLE_1:79; :: thesis: verum