let a be Nat; :: 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 Nat st a in rng $1 holds
a divides Product $1;
A1: 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 A2: S₁[p] ; :: thesis: S₁[p ^ <*n*>]
set p1 = p ^ <*n*>;
A3: rng (p ^ <*n*>) = (rng p) \/ (rng <*n*>) by FINSEQ_1:31;
A4: Product (p ^ <*n*>) = (Product p) * n by RVSUM_1:96;
let a be Nat; :: thesis: ( a in rng (p ^ <*n*>) implies a divides Product (p ^ <*n*>) )
assume A5: a in rng (p ^ <*n*>) ; :: thesis: a divides Product (p ^ <*n*>)

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

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

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

end;

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

then a in {n} by FINSEQ_1:39;
then a = n by TARSKI:def 1;
hence a divides Product (p ^ <*n*>) by A4; :: thesis: verum

end;

end;

end;

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