defpred S₁[ Nat] means for f being FinSequence of NAT
for b being bag of SetPrimes
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: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

A3: 1 <= k + 1 by NAT_1:11;
let f be FinSequence of NAT ; :: thesis: for b being bag of SetPrimes
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 SetPrimes ; :: 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 that
A4: len f = k + 1 and
A5: b is prime-factorization-like and
Product b <> 1 and
A6: a divides Product b and
A7: Product b = Product f and
A8: f = b * (canFS (support b)) ; :: thesis: a in support b
reconsider p = f | k as FinSequence of NAT ;
reconsider x = f . (k + 1) as Element of NAT ;
A9: len p = k by A4, FINSEQ_1:59, NAT_1:11;
A10: f = (f | k) ^ <*(f /. (len f))*> by A4, FINSEQ_5:21
.= p ^ <*x*> by A4, A3, FINSEQ_4:15 ;
then consider p1 being FinSequence of NAT , q being Prime, n being Element of NAT , b1 being bag of SetPrimes such that
0 < n and
A11: b1 is prime-factorization-like and
A12: q in support b and
A13: support b1 = (support b) \ {q} and
A14: x = q |^ n and
A15: len p1 = len p and
A16: Product p = Product p1 and
A17: p1 = b1 * (canFS (support b1)) by A5, A8, Lm5;
A18: Product f = (Product p1) * x by A10, A16, RVSUM_1:96;
rng p1 c= COMPLEX by NUMBERS:20;
then p1 is FinSequence of COMPLEX by FINSEQ_1:def 4;
then A19: Product b1 = Product p1 by A17, NAT_3:def 5;

now :: thesis: a in support b

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

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

a <> 1 by INT_2:def 4;
then ex k being Element of NAT st a = q * k by A6, A7, A14, A18, A20, PEPIN:32;
then A21: q divides a by INT_1:def 3;
q <> 1 by INT_2:def 4;
hence a in support b by A12, A21, INT_2:def 4; :: thesis: verum

end;

suppose A22: 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 A12; :: thesis: verum

end;

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

A24: support b1 c= support b by A13, XBOOLE_1:36;
a in support b1 by A2, A6, A7, A9, A11, A14, A15, A17, A18, A19, A22, A23, Th5;
hence a in support b by A24; :: thesis: verum

end;

end;

end;

end;

end;

hence a in support b ; :: thesis: verum

end;

end;

A25: S₁[ 0 ]

proof

let f be FinSequence of NAT ; :: thesis: for b being bag of SetPrimes
for a being Prime st len f = 0 & 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 SetPrimes ; :: thesis: for a being Prime st len f = 0 & 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 = 0 & 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 len f = 0 ; :: thesis: ( not b is prime-factorization-like or not Product b <> 1 or not a divides Product b or not Product b = Product f or not f = b * (canFS (support b)) or a in support b )
then f = <*> NAT ;
hence ( not b is prime-factorization-like or not Product b <> 1 or not a divides Product b or not Product b = Product f or not f = b * (canFS (support b)) or a in support b ) by RVSUM_1:94; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A25, A1);
hence for i being Element of NAT
for f being FinSequence of NAT
for b being bag of SetPrimes
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