let r1, r2 be set ; ( ( 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 )
( not n >= k & r1 = 0 & r2 = 0 implies r1 = r2 )proof
assume
n >= k
;
( 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:5;
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 !))
;
r1 = r2
r1 = (n !) / ((k !) * (m !))
by A1;
hence
r1 = r2
by A2;
verum
end;
thus
( not n >= k & r1 = 0 & r2 = 0 implies r1 = r2 )
; verum