let p be Prime; :: thesis: for f being FinSequence of SetPrimes st p divides Product f holds
p in rng f
defpred S₁[ FinSequence of SetPrimes ] means for p being Prime st p divides Product $1 holds
p in rng $1;

A1: now

let f be FinSequence of SetPrimes ; :: thesis: for n being Element of SetPrimes st S₁[f] holds
S₁[f ^ <*n*>]
let n be Element of SetPrimes ; :: thesis: ( S₁[f] implies S₁[f ^ <*n*>] )
set f1 = f ^ <*n*>;
assume A2: S₁[f] ; :: thesis: S₁[f ^ <*n*>]
thus S₁[f ^ <*n*>] :: thesis: verum

proof

reconsider nn = n as Nat ;
reconsider ff = f as FinSequence of NAT ;
let p be Prime; :: thesis: ( p divides Product (f ^ <*n*>) implies p in rng (f ^ <*n*>) )
assume p divides Product (f ^ <*n*>) ; :: thesis: p in rng (f ^ <*n*>)
then A3: p divides (Product ff) * n by RVSUM_1:96;

per cases ( p divides Product f or p divides nn ) by A3, NEWTON:80;

suppose A4: p divides Product f ; :: thesis: p in rng (f ^ <*n*>)

A5: rng f c= rng (f ^ <*n*>) by FINSEQ_1:29;
p in rng f by A2, A4;
hence p in rng (f ^ <*n*>) by A5; :: thesis: verum

end;

suppose A6: p divides nn ; :: thesis: p in rng (f ^ <*n*>)

nn is prime by NEWTON:def 6;
then ( p = 1 or p = n ) by A6, INT_2:def 4;
then p in {n} by INT_2:def 4, TARSKI:def 1;
then A7: p in rng <*n*> by FINSEQ_1:38;
rng <*n*> c= rng (f ^ <*n*>) by FINSEQ_1:30;
hence p in rng (f ^ <*n*>) by A7; :: thesis: verum

end;

end;

end;

end;

A8: S₁[ <*> SetPrimes]

proof

let p be Prime; :: thesis: ( p divides Product (<*> SetPrimes) implies p in rng (<*> SetPrimes) )
assume p divides Product (<*> SetPrimes) ; :: thesis: p in rng (<*> SetPrimes)
then p <= 1 by NAT_D:7, RVSUM_1:94;
hence p in rng (<*> SetPrimes) by INT_2:def 4; :: thesis: verum

end;

for p being FinSequence of SetPrimes holds S₁[p] from FINSEQ_2:sch 2(A8, A1);
hence for f being FinSequence of SetPrimes st p divides Product f holds
p in rng f ; :: thesis: verum