for y, x1, x2 being Nat holds
( y = Product ((x2 + 1) + (- (idseq x1))) & x2 > x1 iff ( y = (x1 !) * (x2 choose x1) & x2 > x1 ) ) by Th23;