let n be Nat; :: thesis: Parity ((n + 2) !) = (2 * (Parity (Triangle (n + 1)))) * (Parity (n !))
((n + 1) + 1) ! = ((n + 1) !) * ((n + 1) + 1) by NEWTON:15
.= (n + 2) * ((n !) * (n + 1)) by NEWTON:15
.= (2 * (((n + 1) * ((n + 1) + 1)) / 2)) * (n !)
.= (2 * (Triangle (n + 1))) * (n !) by NUMPOLY1:19 ;
then Parity ((n + 2) !) = (Parity (2 * (Triangle (n + 1)))) * (Parity (n !)) by NEWTON05:25
.= ((Parity 2) * (Parity (Triangle (n + 1)))) * (Parity (n !)) by NEWTON05:25 ;
hence Parity ((n + 2) !) = (2 * (Parity (Triangle (n + 1)))) * (Parity (n !)) ; :: thesis: verum