let a, b, k, l be Nat; :: thesis: ( l > 0 implies ex x being Nat st ((a,b) In_Power (k + l)) . (k + 1) = a * x )
assume l > 0 ; :: thesis: ex x being Nat st ((a,b) In_Power (k + l)) . (k + 1) = a * x
then consider n being Nat such that
A3: l = 1 + n by NAT_1:10, NAT_1:14;
consider x being Nat such that
A4: x = (((k + l) choose k) * (a |^ n)) * (b |^ k) ;
((a,b) In_Power (k + l)) . (k + 1) = (((k + l) choose k) * (a |^ l)) * (b |^ k) by Lm1
.= (((k + l) choose k) * ((a |^ 1) * (a |^ n))) * (b |^ k) by A3, NEWTON:8
.= a * x by A4 ;
hence ex x being Nat st ((a,b) In_Power (k + l)) . (k + 1) = a * x ; :: thesis: verum