let a, b, k, l be Nat; :: thesis: ((a,b) In_Power (k + l)) . (k + 1) = (((k + l) choose k) * (a |^ l)) * (b |^ k)
k + l >= k + 0 by XREAL_1:6;
then ((a,b) In_Power (k + l)) . (k + 1) = (((k + l) choose k) * (a ^ ((k + l) - k))) * (b ^ k) by IRRAT_1:19
.= (((k + l) choose k) * (a |^ l)) * (b |^ k) by POWER:41 ;
hence ((a,b) In_Power (k + l)) . (k + 1) = (((k + l) choose k) * (a |^ l)) * (b |^ k) ; :: thesis: verum