let s be natural Number ; :: thesis: s choose 0 = 1
reconsider m = s - 0 as Element of NAT by ORDINAL1:def 12;
m = s ;
then s choose 0 = (s !) / (1 * (s !)) by Def3, Th12
.= 1 by XCMPLX_1:60 ;
hence s choose 0 = 1 ; :: thesis: verum