let n be Nat; :: thesis: n * (n !) = ((n + 1) !) - (n !)
set a = n ! ;
thus n * (n !) = ((n + 1) * (n !)) - (n !)
.= ((n + 1) !) - (n !) by NEWTON:15 ; :: thesis: verum