let p be bag of ; :: thesis: for X being set st X c= support p holds
ex q, r being bag of 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 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 ) )
assume A1: X c= support p ; :: thesis: ex q, r being bag of 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 )
defpred S₁[ set ] means $1 in X;
deffunc H₁( set ) -> Element of NAT = p . $1;
set fq = p +* (X --> 0 );
A2: dom (X --> 0 ) = X by FUNCOP_1:19;
then A3: dom (p +* (X --> 0 )) = (dom p) \/ X by FUNCT_4:def 1
.= SetPrimes \/ X by PARTFUN1:def 4
.= SetPrimes by A1, XBOOLE_1:1, XBOOLE_1:12 ;
A4: rng p c= NAT by VALUED_0:def 6;
A5: (rng p) \/ (rng (X --> 0 )) c= NAT by A4, XBOOLE_1:8;
rng (p +* (X --> 0 )) c= (rng p) \/ (rng (X --> 0 )) by FUNCT_4:18;
then rng (p +* (X --> 0 )) c= NAT by A5, XBOOLE_1:1;
then reconsider fq = p +* (X --> 0 ) as Function of SetPrimes ,NAT by A3, FUNCT_2:def 1, RELSET_1:11;
A6: 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 A7: x in X ; :: thesis: fq . x = 0
hence fq . x = (X --> 0 ) . x by A2, FUNCT_4:14
.= 0 by A7, FUNCOP_1:13 ;
:: thesis: verum

end;

set fr = p +* ((SetPrimes \ X) --> 0 );
A8: dom (p +* ((SetPrimes \ X) --> 0 )) = (dom p) \/ (dom ((SetPrimes \ X) --> 0 )) by FUNCT_4:def 1
.= (dom p) \/ (SetPrimes \ X) by FUNCOP_1:19
.= SetPrimes \/ (SetPrimes \ X) by PARTFUN1:def 4
.= SetPrimes by XBOOLE_1:12, XBOOLE_1:36 ;
A9: (rng p) \/ (rng ((SetPrimes \ X) --> 0 )) c= NAT by A4, XBOOLE_1:8;
rng (p +* ((SetPrimes \ X) --> 0 )) c= (rng p) \/ (rng ((SetPrimes \ X) --> 0 )) by FUNCT_4:18;
then rng (p +* ((SetPrimes \ X) --> 0 )) c= NAT by A9, XBOOLE_1:1;
then reconsider fr = p +* ((SetPrimes \ X) --> 0 ) as Function of SetPrimes ,NAT by A8, FUNCT_2:def 1, RELSET_1:11;
A10: 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 A11: x in X ; :: thesis: fr . x = p . x
not x in dom ((SetPrimes \ X) --> 0 ) by A11, XBOOLE_0:def 5;
hence fr . x = p . x by FUNCT_4:12; :: thesis: verum

end;

A12: 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 ( not x in X & x in SetPrimes ) ; :: thesis: fr . x = 0
then A13: x in SetPrimes \ X by XBOOLE_0:def 5;
then x in dom ((SetPrimes \ X) --> 0 ) by FUNCOP_1:19;
then fr . x = ((SetPrimes \ X) --> 0 ) . x by FUNCT_4:14;
hence fr . x = 0 by A13, FUNCOP_1:13; :: thesis: verum

end;

A14: 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 A15: ( x in SetPrimes & x in X ) ; :: thesis: fr . x <> 0
then p . x <> 0 by A1, POLYNOM1:def 7;
hence fr . x <> 0 by A10, A15; :: thesis: verum

end;

A16: 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 not x in SetPrimes ; :: thesis: ( fr . x = 0 & fq . x = 0 )
then ( not x in dom fq & not x in dom fr ) ;
hence ( fr . x = 0 & fq . x = 0 ) by FUNCT_1:def 4; :: thesis: verum

end;

A17: 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

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 A12, A14; :: thesis: verum

end;

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

X c= SetPrimes by A1, XBOOLE_1:1;
hence ( x in X iff fr . x <> 0 ) by A16, A18; :: thesis: verum

end;

end;

end;

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

end;

then A19: support fr = X by POLYNOM1:def 7;
A20: 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 A6, XBOOLE_0:def 5; :: thesis: verum

end;

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

then A22: fq . x = p . x by A2, FUNCT_4:12;

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 A21, A22, POLYNOM1: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 A22, POLYNOM1:def 7, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

end;

end;

A23: support fq = (support p) \ X by A20, POLYNOM1:def 7;
A24: (support fq) /\ (support fr) = {}

proof

(support p) \ X misses X by XBOOLE_1:79;
hence (support fq) /\ (support fr) = {} by A19, A23, XBOOLE_0:def 7; :: thesis: verum

end;

then A25: support fq misses support fr by XBOOLE_0:def 7;
A26: fq | (support fq) = p | (support fq)

proof

A27: dom (fq | (support fq)) = (dom fq) /\ (support fq) by RELAT_1:90
.= support fq by POLYNOM1:41, XBOOLE_1:28 ;
A28: dom (p | (support fq)) = (dom p) /\ (support fq) by RELAT_1:90
.= (dom p) /\ ((support p) \ X) by A20, POLYNOM1:def 7
.= ((dom p) /\ (support p)) \ X by XBOOLE_1:49
.= (support p) \ X by POLYNOM1:41, XBOOLE_1:28
.= support fq by A20, POLYNOM1:def 7 ;
A29: 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 ( x in SetPrimes & x in support fq ) ; :: thesis: p . x = fq . x
then not x in X by A19, A24, XBOOLE_0:def 4;
hence p . x = fq . x by A2, FUNCT_4:12; :: 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 A30: x in dom (fq | (support fq)) ; :: thesis: (fq | (support fq)) . x = (p | (support fq)) . x
then ( (fq | (support fq)) . x = fq . x & (p | (support fq)) . x = p . x ) by A27, FUNCT_1:72;
hence (fq | (support fq)) . x = (p | (support fq)) . x by A27, A29, A30; :: thesis: verum

end;

hence fq | (support fq) = p | (support fq) by A27, A28, FUNCT_1:def 17; :: thesis: verum

end;

A31: fr | (support fr) = p | (support fr)

proof

A32: ( support fr c= dom fr & support p c= dom p ) by POLYNOM1:41;
A33: dom (fr | (support fr)) = (dom fr) /\ (support fr) by RELAT_1:90
.= support fr by POLYNOM1:41, XBOOLE_1:28
.= X by A17, POLYNOM1:def 7 ;
A34: dom (p | (support fr)) = (dom p) /\ (support fr) by RELAT_1:90
.= (dom p) /\ X by A17, POLYNOM1:def 7
.= X by A1, A32, XBOOLE_1:1, XBOOLE_1:28 ;
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 A35: x in dom (fr | (support fr)) ; :: thesis: (fr | (support fr)) . x = (p | (support fr)) . x
then ( (fr | (support fr)) . x = fr . x & (p | (support fr)) . x = p . x ) by A19, A33, FUNCT_1:72;
hence (fr | (support fr)) . x = (p | (support fr)) . x by A10, A33, A35; :: thesis: verum

end;

hence fr | (support fr) = p | (support fr) by A33, A34, FUNCT_1:def 17; :: thesis: verum

end;

A36: ( support fq is finite & support fr is finite ) by A1, A19, A20, POLYNOM1:def 7;
reconsider q = fq as bag of by A23, POLYNOM1:def 8;
reconsider r = fr as bag of by A36, POLYNOM1:def 8;
(support fr) \/ (support fq) = (support fr) \/ ((support p) \ (support fr)) by A17, A23, POLYNOM1:def 7
.= (support fr) \/ (support p) by XBOOLE_1:39
.= support p by A1, A19, XBOOLE_1:12 ;
then q + r = p by A24, A26, A31, Th2;
hence ex q, r being bag of 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 A19, A23, A25, A26, A31; :: thesis: verum