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