let r, s be natural Number ; :: thesis: s choose r is Element of NAT
A0: s is Nat by TARSKI:1;
defpred S1[ Nat] means for r being natural Number holds $1 choose r is Element of NAT ;
A1: for s being Nat st S1[s] holds
S1[s + 1]
proof
let s be Nat; :: thesis: ( S1[s] implies S1[s + 1] )
assume A2: S1[s] ; :: thesis: S1[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: S1[ 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 S1[s] from NAT_1:sch 2(A6, A1);
 hence s choose r is Element of NAT by A0; :: thesis: verum