defpred S₁[ Nat] means for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ $1 & Product p = Product q holds
p = q;

A1: now :: thesis:

let k be Nat; :: thesis:
assume A2: S₁[k] ; :: thesis:

now :: thesis:

let p, q be bag of SetPrimes ; :: thesis:
assume that
A3: p is prime-factorization-like and
A4: q is prime-factorization-like and
A5: Product p <= 2 |^ (k + 1) and
A6: Product p = Product q ; :: thesis:

now :: thesis:

per cases ;

suppose A7: support p = {} ; :: thesis:

then Product p = 1 by A3, Th14;
then support q = {} by A4, A6, Th14;
hence p = q by A7, Th4; :: thesis:

end;

suppose support p <> {} ; :: thesis:

then consider x being object such that
A8: x in support p by XBOOLE_0:def 1;
reconsider x = x as Prime by A8, NEWTON:def 6;
A9: x divides Product p by A3, A8, Lm4;
then A10: x in support q by A4, A6, Lm7;

per cases ;

suppose p . x <> x ; :: thesis:

then consider p1, r1 being bag of SetPrimes such that
A11: p1 is prime-factorization-like and
support r1 = {x} and
Product r1 = x and
A12: support p1 = support p and
A13: p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) and
A14: p . x = (p1 . x) * x and
A15: Product p = (Product p1) * x by A3, A8, Lm10;

per cases ;

suppose A16: q . x <> x ; :: thesis:

1 < x by INT_2:def 4;
then 1 + 1 <= x by NAT_1:13;
then A17: (2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by XREAL_1:118;
consider q1, r2 being bag of SetPrimes such that
A18: q1 is prime-factorization-like and
support r2 = {x} and
Product r2 = x and
A19: support q1 = support q and
A20: q1 | ((support q1) \ {x}) = q | ((support q1) \ {x}) and
A21: q . x = (q1 . x) * x and
A22: Product q = (Product q1) * x by A4, A6, A9, A16, Lm7, Lm10;
((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A5, A15, XREAL_1:72;
then ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A17, XXREAL_0:2;
then Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:89;
then Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:8;
then A23: Product p1 <= ((2 |^ k) * 2) / 2 ;
then A24: p1 = q1 by A2, A6, A11, A15, A18, A22, XCMPLX_1:5;

A25: now :: thesis:

let z be set ; :: thesis:
assume A26: z in support p ; :: thesis:

per cases ;

suppose not z in {x} ; :: thesis:

then A27: z in (support p1) \ {x} by A12, A26, XBOOLE_0:def 5;
hence p . z = (p | ((support p1) \ {x})) . z by FUNCT_1:49
.= q . z by A13, A20, A24, A27, FUNCT_1:49 ;
:: thesis:

end;

suppose A28: z in {x} ; :: thesis:

hence p . z = (p1 . x) * x by A14, TARSKI:def 1
.= (q1 . x) * x by A2, A6, A11, A15, A18, A22, A23, XCMPLX_1:5
.= q . z by A21, A28, TARSKI:def 1 ;
:: thesis:

end;

A29: dom p = SetPrimes by PARTFUN1:def 2
.= dom q by PARTFUN1:def 2 ;
support p = support q by A2, A6, A11, A12, A15, A18, A19, A22, A23, XCMPLX_1:5;
then p | (support p) = q | (support q) by A29, A25, FUNCT_1:96;
hence p = q by Th3; :: thesis:

end;

suppose A30: q . x = x ; :: thesis:

1 < x by INT_2:def 4;
then 1 + 1 <= x by NAT_1:13;
then A31: (2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by XREAL_1:118;
((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A5, A15, XREAL_1:72;
then ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A31, XXREAL_0:2;
then Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:89;
then Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:8;
then A32: Product p1 <= ((2 |^ k) * 2) / 2 ;
ex q1, r2 being bag of SetPrimes st
( q1 is prime-factorization-like & support r2 = {x} & Product r2 = x & support q1 = (support q) \ {x} & q1 | (support q1) = q | (support q1) & Product q = (Product q1) * x ) by A4, A6, A9, A30, Lm7, Lm9;
then support p = (support q) \ {x} by A2, A6, A11, A12, A15, A32, XCMPLX_1:5;
then not x in {x} by A8, XBOOLE_0:def 5;
hence p = q by TARSKI:def 1; :: thesis:

end;

suppose A33: p . x = x ; :: thesis:

then consider p1, r1 being bag of SetPrimes such that
A34: p1 is prime-factorization-like and
support r1 = {x} and
Product r1 = x and
A35: support p1 = (support p) \ {x} and
A36: p1 | (support p1) = p | (support p1) and
A37: Product p = (Product p1) * x by A3, A8, Lm9;

per cases ;

suppose A38: q . x <> x ; :: thesis:

1 < x by INT_2:def 4;
then 1 + 1 <= x by NAT_1:13;
then A39: (2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by XREAL_1:118;
((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A5, A37, XREAL_1:72;
then ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A39, XXREAL_0:2;
then Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:89;
then Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:8;
then A40: Product p1 <= ((2 |^ k) * 2) / 2 ;
ex q1, r2 being bag of SetPrimes st
( q1 is prime-factorization-like & support r2 = {x} & Product r2 = x & support q1 = support q & q1 | ((support q1) \ {x}) = q | ((support q1) \ {x}) & q . x = (q1 . x) * x & Product q = (Product q1) * x ) by A4, A6, A9, A38, Lm7, Lm10;
then (support p) \ {x} = support q by A2, A6, A34, A35, A37, A40, XCMPLX_1:5;
then not x in {x} by A10, XBOOLE_0:def 5;
hence p = q by TARSKI:def 1; :: thesis:

end;

suppose A41: q . x = x ; :: thesis:

1 < x by INT_2:def 4;
then 1 + 1 <= x by NAT_1:13;
then A42: (2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by XREAL_1:118;
consider q1, r2 being bag of SetPrimes such that
A43: q1 is prime-factorization-like and
support r2 = {x} and
Product r2 = x and
A44: support q1 = (support q) \ {x} and
A45: q1 | (support q1) = q | (support q1) and
A46: Product q = (Product q1) * x by A4, A6, A9, A41, Lm7, Lm9;
((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A5, A37, XREAL_1:72;
then ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A42, XXREAL_0:2;
then Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:89;
then Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:8;
then A47: Product p1 <= ((2 |^ k) * 2) / 2 ;
then (support p) \ {x} = (support q) \ {x} by A2, A6, A34, A35, A37, A43, A44, A46, XCMPLX_1:5;
then (support p) \/ {x} = ((support q) \ {x}) \/ {x} by XBOOLE_1:39;
then A48: (support p) \/ {x} = (support q) \/ {x} by XBOOLE_1:39;
A49: p1 = q1 by A2, A6, A34, A37, A43, A46, A47, XCMPLX_1:5;

A50: now :: thesis:

let z be set ; :: thesis:
assume A51: z in support p ; :: thesis:

per cases ;

suppose not z in {x} ; :: thesis:

then A52: z in support p1 by A35, A51, XBOOLE_0:def 5;
hence p . z = (p1 | (support p1)) . z by A36, FUNCT_1:49
.= q . z by A45, A49, A52, FUNCT_1:49 ;
:: thesis:

end;

suppose A53: z in {x} ; :: thesis:

hence p . z = x by A33, TARSKI:def 1
.= q . z by A41, A53, TARSKI:def 1 ;
:: thesis:

end;

A54: {x} c= support q by A10, ZFMISC_1:31;
{x} c= support p by A8, ZFMISC_1:31;
then A55: support p = (support q) \/ {x} by A48, XBOOLE_1:12;
dom p = SetPrimes by PARTFUN1:def 2
.= dom q by PARTFUN1:def 2 ;
then p | (support p) = q | (support p) by A50, FUNCT_1:96
.= q | (support q) by A54, A55, XBOOLE_1:12 ;
hence p = q by Th3; :: thesis:

end;

hence p = q ; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A56: S₁[ 0 ]

proof

let p, q be bag of SetPrimes ; :: thesis:
assume that
A57: p is prime-factorization-like and
A58: q is prime-factorization-like and
A59: Product p <= 2 |^ 0 and
A60: Product p = Product q ; :: thesis:
Product p <> 0 by A57, Th13;
then A61: 0 + 1 <= Product p by NAT_1:13;
Product p <= 1 by A59, NEWTON:4;
then A62: Product p = 1 by A61, XXREAL_0:1;
then A63: support p = {} by A57, Th14;
support q = {} by A58, A60, A62, Th14;
hence p = q by A63, Th4; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A56, A1);
hence for n being Element of NAT
for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ n & Product p = Product q holds
p = q ; :: thesis: