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