let s be Nat; :: thesis: s choose 0 = 1
reconsider m = s - 0 as Element of NAT by ORDINAL1:def 13;
A1: s ! <> 0 by Th23;
m = s ;
then s choose 0 = (s ! ) / (1 * (s ! )) by Def3, Th18
.= 1 by A1, XCMPLX_1:60 ;
hence s choose 0 = 1 ; :: thesis: verum