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