let fp be FinSequence of NAT ; :: thesis: for a being Nat st a in dom fp holds
fp . a divides Product fp
let a be Nat; :: thesis: ( a in dom fp implies fp . a divides Product fp )
assume a in dom fp ; :: thesis: fp . a divides Product fp
then fp . a in rng fp by FUNCT_1:3;
hence fp . a divides Product fp by NAT_3:7; :: thesis: verum