( 1 + 0 <= 1 + k & (k + 1) + 0 <= (k + 1) + l ) by XREAL_1:6;
then ( 1 <= k + 1 & k + 1 <= len ((a,b) Subnomial (((k + l) + 1) - 1)) ) ;
then ( k = (k + 1) - 1 & l = (k + l) - k & k + 1 in dom ((a,b) Subnomial (k + l)) ) by FINSEQ_3:25;
then ((a,b) Subnomial (k + l)) . (k + 1) = (a |^ l) * (b |^ k) by Def2;
hence ((a,b) Subnomial (k + l)) . (k + 1) is positive ; :: thesis: verum