let a be natural number ; :: thesis: for f being FinSequence of NAT st a in rng f holds
a divides Product f
defpred S₁[ FinSequence of NAT ] means for a being natural number st a in rng $1 holds
a divides Product $1;
A1: S₁[ <*> NAT ] ;
A2: for p being FinSequence of NAT
for n being Element of NAT st S₁[p] holds
S₁[p ^ <*n*>]

proof

let p be FinSequence of NAT ; :: thesis: for n being Element of NAT st S₁[p] holds
S₁[p ^ <*n*>]
let n be Element of NAT ; :: thesis: ( S₁[p] implies S₁[p ^ <*n*>] )
assume A3: S₁[p] ; :: thesis: S₁[p ^ <*n*>]
set p1 = p ^ <*n*>;
let a be natural number ; :: thesis: ( a in rng (p ^ <*n*>) implies a divides Product (p ^ <*n*>) )
assume A4: a in rng (p ^ <*n*>) ; :: thesis: a divides Product (p ^ <*n*>)
A5: rng (p ^ <*n*>) = (rng p) \/ (rng <*n*>) by FINSEQ_1:44;
A6: Product (p ^ <*n*>) = (Product p) * n by RVSUM_1:126;

per cases ( a in rng p or a in rng <*n*> ) by A4, A5, XBOOLE_0:def 3;

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

hence a divides Product (p ^ <*n*>) by A3, A6, NAT_D:9; :: thesis: verum

end;

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

then a in {n} by FINSEQ_1:56;
then a = n by TARSKI:def 1;
hence a divides Product (p ^ <*n*>) by A6, NAT_D:9; :: thesis: verum

end;

end;

end;

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