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 {x} c= support p by ZFMISC_1:37;
then consider q, r being bag of such that
A2: ( 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;
A3: (Product q) * (Product r) = Product p by A2, NAT_3:19;
defpred S₁[ set ] means $1 in {x};
consider nx being natural number such that
A4: ( 0 < nx & p . x = x |^ nx ) by A1, Def1;
consider mx being Nat such that
A5: nx = mx + 1 by A4, NAT_1:6;
A6: mx = 0

proof

assume mx <> 0 ; :: thesis:
then 0 < mx ;
then A7: 0 + 1 < mx + 1 by XREAL_1:10;
1 < x by INT_2:def 5;
then A8: x to_power 1 < x to_power nx by A5, A7, POWER:44;
x |^ 1 < x to_power nx by A8, POWER:46;
then x |^ 1 < x |^ nx by POWER:46;
hence contradiction by A1, A4, NEWTON:10; :: thesis:

end;

A9: q is prime-factorization-like

proof

now

let z be Prime; :: thesis:
assume A10: z in support q ; :: thesis:
A11: support q c= support p by A2, XBOOLE_1:36;
consider n being natural number such that
A12: ( 0 < n & p . z = z |^ n ) by A1, A10, A11, Def1;
take n = n; :: thesis:
q . z = (q | (support q)) . z by A10, FUNCT_1:72
.= p . z by A2, A10, FUNCT_1:72 ;
hence ( 0 < n & q . z = z |^ n ) by A12; :: thesis:

end;

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

end;

A13: x in support r by A2, TARSKI:def 1;
A14: r . x = (r | (support r)) . x by A13, FUNCT_1:72
.= p . x by A2, A13, FUNCT_1:72
.= x by A4, A5, A6, NEWTON:10 ;
r = (SetPrimes --> 0 ) +* x,(r . x) by A2, Th1;
then ex rr1 being bag of st
( rr1 = r & support rr1 = {x} & Product rr1 = x ) by A14, Lm8;
hence ex p1, r1 being bag of st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = (support p) \ {x} & p1 | (support p1) = p | (support p1) & Product p = (Product p1) * x ) by A2, A3, A9; :: thesis: