let n, k be Nat; :: thesis: for p being Prime st k < p holds
(((n * p) + k) choose (n * p)) mod p = 1
let p be Prime; :: thesis: ( k < p implies (((n * p) + k) choose (n * p)) mod p = 1 )
assume A1: k < p ; :: thesis: (((n * p) + k) choose (n * p)) mod p = 1
(((n * p) + k) choose k) mod p = 1 by A1, NPK;
hence (((n * p) + k) choose (n * p)) mod p = 1 by N20; :: thesis: verum