let p be bag of SetPrimes ; :: thesis: for x being Prime st p is prime-factorization-like & x in support p & p . x = x holds
ex p1, r1 being bag of SetPrimes 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 )
let x be Prime; :: thesis: ( p is prime-factorization-like & x in support p & p . x = x implies ex p1, r1 being bag of SetPrimes 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 ) )
assume that
A1: p is prime-factorization-like and
A2: x in support p and
A3: p . x = x ; :: thesis: ex p1, r1 being bag of SetPrimes 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 )
consider nx being Nat such that
A4: 0 < nx and
A5: p . x = x |^ nx by A1, A2;
consider mx being Nat such that
A6: nx = mx + 1 by A4, NAT_1:6;
A7: mx = 0

proof

assume mx <> 0 ; :: thesis: contradiction
then A8: 0 + 1 < mx + 1 by XREAL_1:8;
1 < x by INT_2:def 4;
then x to_power 1 < x to_power nx by A6, A8, POWER:39;
then x |^ 1 < x to_power nx by POWER:41;
then x |^ 1 < x |^ nx by POWER:41;
hence contradiction by A3, A5; :: thesis: verum

end;

{x} c= support p by A2, ZFMISC_1:31;
then consider q, r being bag of SetPrimes such that
A9: support q = (support p) \ {x} and
A10: support r = {x} and
A11: support q misses support r and
A12: q | (support q) = p | (support q) and
A13: r | (support r) = p | (support r) and
A14: q + r = p by Lm3;
A15: r = (SetPrimes --> 0) +* (x,(r . x)) by A10, Th1;

now :: thesis: for z being Prime st z in support q holds
ex n being Nat st
( 0 < n & q . z = z |^ n )

let z be Prime; :: thesis: ( z in support q implies ex n being Nat st
( 0 < n & q . z = z |^ n ) )
assume A16: z in support q ; :: thesis: ex n being Nat st
( 0 < n & q . z = z |^ n )
support q c= support p by A9, XBOOLE_1:36;
then consider n being Nat such that
A17: 0 < n and
A18: p . z = z |^ n by A1, A16;
take n = n; :: thesis: ( 0 < n & q . z = z |^ n )
q . z = (q | (support q)) . z by A16, FUNCT_1:49
.= p . z by A12, A16, FUNCT_1:49 ;
hence ( 0 < n & q . z = z |^ n ) by A17, A18; :: thesis: verum

end;

then A19: q is prime-factorization-like ;
A20: x in support r by A10, TARSKI:def 1;
then r . x = (r | (support r)) . x by FUNCT_1:49
.= p . x by A13, A20, FUNCT_1:49
.= x by A5, A6, A7 ;
then A21: ex rr1 being bag of SetPrimes st
( rr1 = r & support rr1 = {x} & Product rr1 = x ) by A15, Lm8;
(Product q) * (Product r) = Product p by A11, A14, NAT_3:19;
hence ex p1, r1 being bag of SetPrimes 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 A9, A12, A19, A21; :: thesis: verum