let a, b, k, l be Nat; ( k + l is prime & k > 0 & l > 0 implies k + l divides ((a,b) In_Power (k + l)) . (k + 1) )
assume A1:
( k + l is prime & k > 0 & l > 0 )
; k + l divides ((a,b) In_Power (k + l)) . (k + 1)
then
k + l > k + 0
by XREAL_1:6;
then A2:
k + l divides (k + l) choose k
by A1, Th21;
(k + l) choose k divides ((k + l) choose k) * ((a |^ l) * (b |^ k))
;
then consider x being Nat such that
A3:
((k + l) choose k) * ((a |^ l) * (b |^ k)) = (k + l) * x
by A2, INT_2:9, NAT_D:def 3;
((a,b) In_Power (k + l)) . (k + 1) =
(((k + l) choose k) * (a |^ l)) * (b |^ k)
by Lm1
.=
(k + l) * x
by A3
;
hence
k + l divides ((a,b) In_Power (k + l)) . (k + 1)
; verum