(4 + 1) ! = (4 + 1) * (4 ! ) by NEWTON:21
.= 5 * ((3 + 1) * (3 ! )) by NEWTON:21
.= 5 * (4 * ((2 + 1) * (2 ! ))) by NEWTON:21
.= 120 by NEWTON:20 ;
hence (4 + 1) ! = 120 ; :: thesis: verum