let r, s be natural Number ; :: thesis: s choose r is Element of NAT
A0: s is Nat by TARSKI:1;
defpred S₁[ Nat] means for r being natural Number holds $1 choose r is Element of NAT ;
A1: for s being Nat st S₁[s] holds
S₁[s + 1]

proof

let s be Nat; :: thesis: ( S₁[s] implies S₁[s + 1] )
assume A2: S₁[s] ; :: thesis: S₁[s + 1]
A3: for r being natural Number st r <> 0 holds
(s + 1) choose r is Element of NAT

proof

let r be natural Number ; :: thesis: ( r <> 0 implies (s + 1) choose r is Element of NAT )
assume A4: r <> 0 ; :: thesis: (s + 1) choose r is Element of NAT
(s + 1) choose r is Element of NAT

proof

consider t being Nat such that
A5: r = t + 1 by A4, NAT_1:6;
reconsider t = t as Element of NAT by ORDINAL1:def 12;
reconsider m1 = s choose t, m2 = s choose (t + 1) as Element of NAT by A2;
m1 + m2 = (s choose t) + (s choose (t + 1)) ;
hence (s + 1) choose r is Element of NAT by A5, Th22; :: thesis: verum

end;

hence (s + 1) choose r is Element of NAT ; :: thesis: verum

end;

let r be natural Number ; :: thesis: (s + 1) choose r is Element of NAT
( r = 0 or r <> 0 ) ;
hence (s + 1) choose r is Element of NAT by A3, Th19; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

let r be natural Number ; :: thesis: 0 choose r is Element of NAT
( r = 0 or r > 0 ) ;
hence 0 choose r is Element of NAT by Def3, Th19; :: thesis: verum

end;

for s being Nat holds S₁[s] from NAT_1:sch 2(A6, A1);
hence s choose r is Element of NAT by A0; :: thesis: verum