let n be even Nat; :: thesis: Parity (n !) = Parity ((n + 1) !)
Parity (n + 1) = 1 by NAT_2:def 1;
then Parity ((n + 1) !) = 1 * (Parity (n !)) by PAS;
hence Parity (n !) = Parity ((n + 1) !) ; :: thesis: verum