let r1, r2 be set ; :: thesis: ( ( n >= k & ( for l being Nat st l = n - k holds
r1 = (n ! ) / ((k ! ) * (l ! )) ) & ( for l being Nat st l = n - k holds
r2 = (n ! ) / ((k ! ) * (l ! )) ) implies r1 = r2 ) & ( not n >= k & r1 = 0 & r2 = 0 implies r1 = r2 ) )
thus ( n >= k & ( for l being Nat st l = n - k holds
r1 = (n ! ) / ((k ! ) * (l ! )) ) & ( for l being Nat st l = n - k holds
r2 = (n ! ) / ((k ! ) * (l ! )) ) implies r1 = r2 ) :: thesis: ( not n >= k & r1 = 0 & r2 = 0 implies r1 = r2 )

proof

assume A1: n >= k ; :: thesis: ( ex l being Nat st
( l = n - k & not r1 = (n ! ) / ((k ! ) * (l ! )) ) or ex l being Nat st
( l = n - k & not r2 = (n ! ) / ((k ! ) * (l ! )) ) or r1 = r2 )
assume A2: ( ( for l being Nat st l = n - k holds
r1 = (n ! ) / ((k ! ) * (l ! )) ) & ( for l being Nat st l = n - k holds
r2 = (n ! ) / ((k ! ) * (l ! )) ) ) ; :: thesis: r1 = r2
reconsider m = n - k as Element of NAT by A1, INT_1:18;
( r1 = (n ! ) / ((k ! ) * (m ! )) & r2 = (n ! ) / ((k ! ) * (m ! )) ) by A2;
hence r1 = r2 ; :: thesis: verum

end;

thus ( not n >= k & r1 = 0 & r2 = 0 implies r1 = r2 ) ; :: thesis: verum