let p be Prime; :: thesis: for n being Nat holds (n choose (p - 1)) mod p = ((n mod p) choose (p - 1)) mod p
let n be Nat; :: thesis: (n choose (p - 1)) mod p = ((n mod p) choose (p - 1)) mod p
(p - 1) + 0 < (p - 1) + 1 by XREAL_1:6;
hence (n choose (p - 1)) mod p = ((n mod p) choose (p - 1)) mod p by MOC; :: thesis: verum