theorem PAS: :: NEWTON07:45

for n being Nat holds Parity ((n + 1) !) = (Parity (n + 1)) * (Parity (n !))