let p be bag of ; :: thesis:
let x be Prime; :: thesis:
assume A1: ( p is prime-factorization-like & x in support p & p . x <> x ) ; :: thesis:
then A2: {x} c= support p by ZFMISC_1:37;
then consider q, r being bag of such that
A3: ( 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 Lm3;
defpred S₁[ set ] means $1 in {x};
A4: (support q) /\ (support r) = {} by A3, XBOOLE_0:def 7;
set r10 = (SetPrimes --> 0 ) +* x,x;
consider nx being natural number such that
A5: ( 0 < nx & p . x = x |^ nx ) by A1, Def1;
consider mx being Nat such that
A6: nx = mx + 1 by A5, NAT_1:6;
A7: mx <> 0 by A1, A5, A6, NEWTON:10;
A8: x in support r by A3, TARSKI:def 1;
A9: r . x = (r | (support r)) . x by A8, FUNCT_1:72
.= p . x by A3, A8, FUNCT_1:72 ;
A10: (r . x) / x = ((x |^ mx) * x) / x by A5, A6, A9, NEWTON:11
.= x |^ mx by XCMPLX_1:90 ;
reconsider rxx = (r . x) / x as Element of NAT by A10, ORDINAL1:def 13;
defpred S₂[ set ] means $1 in {x};
set r20 = (SetPrimes --> 0 ) +* x,rxx;
( x is Element of NAT & x <> 0 ) by ORDINAL1:def 13;
then consider r1 being bag of such that
A11: ( r1 = (SetPrimes --> 0 ) +* x,x & support r1 = {x} & Product r1 = x ) by Lm8;
rxx <> 0

proof

assume A12: rxx = 0 ; :: thesis:
r . x = rxx * x by XCMPLX_1:88
.= 0 by A12 ;
hence contradiction by A5, A9; :: thesis:

end;

then consider r2 being bag of such that
A13: ( r2 = (SetPrimes --> 0 ) +* x,rxx & support r2 = {x} & Product r2 = rxx ) by Lm8;
A14: r . x = rxx * x by XCMPLX_1:88;
r = (SetPrimes --> 0 ) +* x,(r . x) by A3, Th1;
then A15: ex rr1 being bag of st
( rr1 = r & support rr1 = {x} & Product rr1 = rxx * x ) by A5, A9, A14, Lm8;
A16: dom (SetPrimes --> 0 ) = SetPrimes by FUNCOP_1:19;
then A17: x in dom (SetPrimes --> 0 ) by NEWTON:def 6;
set p1 = q + r2;
x in {x} by TARSKI:def 1;
then A18: not x in support q by A3, XBOOLE_0:def 5;
(q + r2) . x = (q . x) + (r2 . x) by POLYNOM1:def 5
.= 0 + (r2 . x) by A18, POLYNOM1:def 7
.= rxx by A13, A17, FUNCT_7:33 ;
then A19: p . x = ((q + r2) . x) * x by A9, XCMPLX_1:88;
A20: Product p = (Product q) * ((Product r2) * x) by A3, A13, A15, NAT_3:19
.= ((Product q) * (Product r2)) * x
.= (Product (q + r2)) * x by A3, A13, NAT_3:19 ;
A21: q + r2 is prime-factorization-like

proof

now

let z be Prime; :: thesis:
assume z in support (q + r2) ; :: thesis:
then A22: z in (support q) \/ (support r2) by POLYNOM1:42;
A23: (q + r2) . z = (q . z) + (r2 . z) by POLYNOM1:def 5;

per cases by A22, XBOOLE_0:def 3;

suppose A24: z in support q ; :: thesis:

support q c= support p by A3, XBOOLE_1:36;
then consider n being natural number such that
A25: ( 0 < n & p . z = z |^ n ) by A1, A24, Def1;
A26: q . z = (q | (support q)) . z by A24, FUNCT_1:72
.= p . z by A3, A24, FUNCT_1:72 ;
not z in {x} by A3, A24, XBOOLE_0:def 5;
then A27: r2 . z = 0 by A13, POLYNOM1:def 7;
thus ex n being natural number st
( 0 < n & (q + r2) . z = z |^ n ) by A23, A25, A26, A27; :: thesis:

end;

suppose A28: z in support r2 ; :: thesis:

then A29: z = x by A13, TARSKI:def 1;
A30: not z in support q by A3, A4, A13, A28, XBOOLE_0:def 4;
take mx = mx; :: thesis:
thus 0 < mx by A7; :: thesis:
(q + r2) . z = (q . z) + (r2 . z) by POLYNOM1:def 5
.= 0 + (r2 . z) by A30, POLYNOM1:def 7
.= z |^ mx by A10, A13, A16, A28, A29, FUNCT_7:33 ;
hence (q + r2) . z = z |^ mx ; :: thesis:

end;

hence q + r2 is prime-factorization-like by Def1; :: thesis:

end;

A31: dom (q + r2) = SetPrimes by PARTFUN1:def 4
.= dom p by PARTFUN1:def 4 ;

now

let z be set ; :: thesis:
assume A32: z in (support (q + r2)) \ {x} ; :: thesis:
then z in support (q + r2) by XBOOLE_0:def 5;
then z in (support q) \/ (support r2) by POLYNOM1:42;
then A33: ( z in support q or z in support r2 ) by XBOOLE_0:def 3;
A34: (q + r2) . z = (q . z) + (r2 . z) by POLYNOM1:def 5;
A35: q . z = (q | (support q)) . z by A13, A32, A33, FUNCT_1:72, XBOOLE_0:def 5
.= p . z by A3, A13, A32, A33, FUNCT_1:72, XBOOLE_0:def 5 ;
not z in {x} by A32, XBOOLE_0:def 5;
then r2 . z = 0 by A13, POLYNOM1:def 7;
hence (q + r2) . z = p . z by A34, A35; :: thesis:

end;

then A36: (q + r2) | ((support (q + r2)) \ {x}) = p | ((support (q + r2)) \ {x}) by A31, FUNCT_1:166;
support (q + r2) = ((support p) \ {x}) \/ {x} by A3, A13, POLYNOM1:42
.= (support p) \/ {x} by XBOOLE_1:39
.= support p by A2, XBOOLE_1:12 ;
hence ex p1, r1 being bag of st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x ) by A11, A19, A20, A21, A36; :: thesis: