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 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 )
then reconsider m = n - k as Element of NAT by INT_1:18;
assume that
A1: for l being Nat st l = n - k holds
r1 = (n ! ) / ((k ! ) * (l ! )) and
A2: for l being Nat st l = n - k holds
r2 = (n ! ) / ((k ! ) * (l ! )) ; :: thesis: r1 = r2
r1 = (n ! ) / ((k ! ) * (m ! )) by A1;
hence r1 = r2 by A2; :: thesis: verum

end;

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