let p be Prime; :: thesis: for f being FinSequence of NAT st f is positive-yielding & p divides Product f holds
ex i being Nat st
( i in dom f & p divides f . i )
defpred S₁[ Nat] means for f being FinSequence of NAT st len f = $1 & f is positive-yielding & p divides Product f holds
ex i being Nat st
( i in dom f & p divides f . i );
A1: S₁[ 0 ]

proof

let f be FinSequence of NAT ; :: thesis: ( len f = 0 & f is positive-yielding & p divides Product f implies ex i being Nat st
( i in dom f & p divides f . i ) )
assume A2: ( len f = 0 & f is positive-yielding & p divides Product f ) ; :: thesis: ex i being Nat st
( i in dom f & p divides f . i )
f = <*> REAL by A2;
hence ex i being Nat st
( i in dom f & p divides f . i ) by INT_2:def 4, A2, INT_2:27, RVSUM_1:94; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let f be FinSequence of NAT ; :: thesis: ( len f = n + 1 & f is positive-yielding & p divides Product f implies ex i being Nat st
( i in dom f & p divides f . i ) )
assume A5: ( len f = n + 1 & f is positive-yielding & p divides Product f ) ; :: thesis: ex i being Nat st
( i in dom f & p divides f . i )
f = (f | n) ^ <*(f . (n + 1))*> by A5, FINSEQ_3:55;
then Product f = (Product (f | n)) * (f . (n + 1)) by RVSUM_1:96;

per cases then ( p divides f . (n + 1) or p divides Product (f | n) ) by NEWTON:80, A5;

suppose A6: p divides f . (n + 1) ; :: thesis: ex i being Nat st
( i in dom f & p divides f . i )

1 <= n + 1 by NAT_1:11;
hence ex i being Nat st
( i in dom f & p divides f . i ) by A6, A5, FINSEQ_3:25; :: thesis: verum

end;

suppose A7: p divides Product (f | n) ; :: thesis: ex i being Nat st
( i in dom f & p divides f . i )

len (f | n) = n by A5, FINSEQ_1:59, NAT_1:11;
then consider i being Nat such that
A8: ( i in dom (f | n) & p divides (f | n) . i ) by A7, A4, A5;
( i in dom f & (f | n) . i = f . i ) by A8, FUNCT_1:47, RELAT_1:57;
hence ex i being Nat st
( i in dom f & p divides f . i ) by A8; :: thesis: verum

end;

end;

end;

let f be FinSequence of NAT ; :: thesis: ( f is positive-yielding & p divides Product f implies ex i being Nat st
( i in dom f & p divides f . i ) )
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
then S₁[ len f] ;
hence ( f is positive-yielding & p divides Product f implies ex i being Nat st
( i in dom f & p divides f . i ) ) ; :: thesis: verum