let a, b, k, l, n be Nat; :: thesis: ( n = ((a,b) In_Power (k + l)) . (k + 1) & l > 0 implies a divides n )
assume ( n = ((a,b) In_Power (k + l)) . (k + 1) & l > 0 ) ; :: thesis: a divides n
then consider x being Nat such that
A2: n = a * x by Th50;
thus a divides n by A2; :: thesis: verum