for x1, w, u being Nat st x1 * w,1 are_congruent_mod u holds
for x being Nat holds Product (1 + (x1 * (idseq x))),((x1 |^ x) * (x !)) * ((w + x) choose x) are_congruent_mod u