defpred S₁[ Element of 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: S₁[ 0 ]

proof

let p, q be bag of SetPrimes ; :: thesis: ( p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ 0 & Product p = Product q implies p = q )
assume A2: ( p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ 0 & Product p = Product q ) ; :: thesis: p = q
A3: Product p <= 1 by A2, NEWTON:9;
Product p <> 0 by A2, Th13;
then 0 < Product p ;
then 0 + 1 <= Product p by NAT_1:13;
then A4: Product p = 1 by A3, XXREAL_0:1;
then A5: support p = {} by A2, Th14;
support q = {} by A2, A4, Th14;
hence p = q by A5, Th4; :: thesis: verum

end;

A6: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]

now

let p, q be bag of SetPrimes ; :: thesis: ( p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ (k + 1) & Product p = Product q implies p = q )
assume A8: ( p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ (k + 1) & Product p = Product q ) ; :: thesis: p = q

now

per cases ( support p = {} or support p <> {} ) ;

suppose A9: support p = {} ; :: thesis: p = q

then Product p = 1 by A8, Th14;
then support q = {} by A8, Th14;
hence p = q by A9, Th4; :: thesis: verum

end;

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

then consider x being set such that
A10: x in support p by XBOOLE_0:def 1;
x is Element of SetPrimes by A10;
then reconsider x = x as Prime by NEWTON:def 6;
x divides Product p by A8, A10, Lm4;
then A11: x in support q by A8, Lm7;

per cases ( p . x <> x or p . x = x ) ;

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

then consider p1, r1 being bag of SetPrimes such that
A12: ( 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 A8, A10, Lm10;

per cases ( q . x <> x or q . x = x ) ;

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

then consider q1, r2 being bag of SetPrimes such that
A13: ( 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 A8, A11, Lm10;
A14: 1 < x by INT_2:def 5;
A15: 1 + 1 <= x by A14, NAT_1:13;
A16: ((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A8, A12, XREAL_1:74;
(2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by A15, XREAL_1:120;
then ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A16, XXREAL_0:2;
then Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:90;
then Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:13;
then A17: Product p1 <= ((2 |^ k) * 2) / 2 by NEWTON:10;
A18: p1 = q1 by A7, A8, A12, A13, A17, XCMPLX_1:5;
A19: support p = support q by A7, A8, A12, A13, A17, XCMPLX_1:5;
A20: dom p = SetPrimes by PBOOLE:def 3
.= dom q by PBOOLE:def 3 ;

now

let z be set ; :: thesis: ( z in support p implies p . b₁ = q . b₁ )
assume A21: z in support p ; :: thesis: p . b₁ = q . b₁

per cases ( not z in {x} or z in {x} ) ;

suppose not z in {x} ; :: thesis: p . b₁ = q . b₁

then A22: z in (support p1) \ {x} by A12, A21, XBOOLE_0:def 5;
thus p . z = (p | ((support p1) \ {x})) . z by A22, FUNCT_1:72
.= q . z by A12, A13, A18, A22, FUNCT_1:72 ; :: thesis: verum

end;

suppose A23: z in {x} ; :: thesis: p . b₁ = q . b₁

thus p . z = (p1 . x) * x by A12, A23, TARSKI:def 1
.= (q1 . x) * x by A7, A8, A12, A13, A17, XCMPLX_1:5
.= q . z by A13, A23, TARSKI:def 1 ; :: thesis: verum

end;

end;

end;

then p | (support p) = q | (support q) by A19, A20, FUNCT_1:166;
hence p = q by Th3; :: thesis: verum

end;

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

then consider q1, r2 being bag of SetPrimes such that
A24: ( 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 A8, A11, Lm9;
A25: 1 < x by INT_2:def 5;
A26: 1 + 1 <= x by A25, NAT_1:13;
A27: ((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A8, A12, XREAL_1:74;
(2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by A26, XREAL_1:120;
then ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A27, XXREAL_0:2;
then Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:90;
then Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:13;
then A28: Product p1 <= ((2 |^ k) * 2) / 2 by NEWTON:10;
A29: support p = (support q) \ {x} by A7, A8, A12, A24, A28, XCMPLX_1:5;
( x in support q & not x in {x} ) by A10, A29, XBOOLE_0:def 5;
hence p = q by TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

then consider p1, r1 being bag of SetPrimes such that
A31: ( 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 A8, A10, Lm9;

per cases ( q . x <> x or q . x = x ) ;

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

then consider q1, r2 being bag of SetPrimes such that
A32: ( 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 A8, A11, Lm10;
A33: 1 < x by INT_2:def 5;
A34: 1 + 1 <= x by A33, NAT_1:13;
A35: ((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A8, A31, XREAL_1:74;
(2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by A34, XREAL_1:120;
then ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A35, XXREAL_0:2;
then Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:90;
then Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:13;
then A36: Product p1 <= ((2 |^ k) * 2) / 2 by NEWTON:10;
A37: (support p) \ {x} = support q by A7, A8, A31, A32, A36, XCMPLX_1:5;
( x in support p & not x in {x} ) by A11, A37, XBOOLE_0:def 5;
hence p = q by TARSKI:def 1; :: thesis: verum

end;

suppose A38: q . x = x ; :: thesis: p = q

then consider q1, r2 being bag of SetPrimes such that
A39: ( 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 A8, A11, Lm9;
A40: 1 < x by INT_2:def 5;
A41: 1 + 1 <= x by A40, NAT_1:13;
A42: ((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A8, A31, XREAL_1:74;
(2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by A41, XREAL_1:120;
then ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A42, XXREAL_0:2;
then Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:90;
then Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:13;
then A43: Product p1 <= ((2 |^ k) * 2) / 2 by NEWTON:10;
A44: p1 = q1 by A7, A8, A31, A39, A43, XCMPLX_1:5;
(support p) \ {x} = (support q) \ {x} by A7, A8, A31, A39, A43, XCMPLX_1:5;
then (support p) \/ {x} = ((support q) \ {x}) \/ {x} by XBOOLE_1:39;
then A45: (support p) \/ {x} = (support q) \/ {x} by XBOOLE_1:39;
A46: {x} c= support p by A10, ZFMISC_1:37;
A47: {x} c= support q by A11, ZFMISC_1:37;
A48: support p = (support q) \/ {x} by A45, A46, XBOOLE_1:12;
A49: dom p = SetPrimes by PBOOLE:def 3
.= dom q by PBOOLE:def 3 ;

now

let z be set ; :: thesis: ( z in support p implies p . b₁ = q . b₁ )
assume A50: z in support p ; :: thesis: p . b₁ = q . b₁

per cases ( not z in {x} or z in {x} ) ;

suppose not z in {x} ; :: thesis: p . b₁ = q . b₁

then A51: z in support p1 by A31, A50, XBOOLE_0:def 5;
thus p . z = (p1 | (support p1)) . z by A31, A51, FUNCT_1:72
.= q . z by A39, A44, A51, FUNCT_1:72 ; :: thesis: verum

end;

suppose A52: z in {x} ; :: thesis: p . b₁ = q . b₁

thus p . z = x by A30, A52, TARSKI:def 1
.= q . z by A38, A52, TARSKI:def 1 ; :: thesis: verum

end;

end;

end;

then p | (support p) = q | (support p) by A49, FUNCT_1:166
.= q | (support q) by A47, A48, XBOOLE_1:12 ;
hence p = q by Th3; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

hence p = q ; :: thesis: verum

end;

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A6);
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: verum