defpred S₁[ Element of NAT ] means for f being FinSequence of NAT
for b being bag of
for a being Prime st len f = $1 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b;
A1: S₁[ 0 ] by FINSEQ_1:32, RVSUM_1:124;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

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

proof

let f be FinSequence of NAT ; :: thesis: for b being bag of
for a being Prime st len f = k + 1 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let b be bag of ; :: thesis: for a being Prime st len f = k + 1 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let a be Prime; :: thesis: ( len f = k + 1 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) implies a in support b )
assume A4: ( len f = k + 1 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) ) ; :: thesis: a in support b
reconsider x = f . (k + 1) as Element of NAT ;
reconsider p = f | k as FinSequence of NAT ;
A5: ( 1 <= k + 1 & k + 1 <= len f ) by A4, NAT_1:11;
A6: f = (f | k) ^ <*(f /. (len f))*> by A4, FINSEQ_5:24
.= p ^ <*x*> by A4, A5, FINSEQ_4:24 ;
A7: len p = k by A4, FINSEQ_1:80, NAT_1:11;
consider p1 being FinSequence of NAT , q being Prime, n being Element of NAT , b1 being bag of such that
A8: ( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) ) by A4, A6, Lm5;
A9: Product f = (Product p1) * x by A6, A8, RVSUM_1:126;
rng p1 c= COMPLEX by NUMBERS:20, XBOOLE_1:1;
then p1 is FinSequence of COMPLEX by FINSEQ_1:def 4;
then A10: Product b1 = Product p1 by A8, NAT_3:def 5;

now

per cases ( Product p1 = 1 or Product p1 <> 1 ) ;

suppose A11: Product p1 = 1 ; :: thesis: a in support b

A12: ( a <> 1 & q <> 1 ) by INT_2:def 5;
then ex k being Element of NAT st a = q * k by A4, A8, A9, A11, PEPIN:33;
then q divides a by INT_1:def 9;
hence a in support b by A8, A12, INT_2:def 5; :: thesis: verum

end;

suppose A13: Product p1 <> 1 ; :: thesis: a in support b

per cases ( a = q or a <> q ) ;

suppose a = q ; :: thesis: a in support b

hence a in support b by A8; :: thesis: verum

end;

suppose A14: a <> q ; :: thesis: a in support b

A15: a in support b1 by A3, A4, A7, A8, A9, A10, A13, A14, Th5;
support b1 c= support b by A8, XBOOLE_1:36;
hence a in support b by A15; :: thesis: verum

end;

end;

end;

end;

end;

hence a in support b ; :: thesis: verum

end;

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
hence for i being Element of NAT
for f being FinSequence of NAT
for b being bag of
for a being Prime st len f = i & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b ; :: thesis: verum