per cases ( k in dom ((a,b) In_Power n) or not k in dom ((a,b) In_Power n) ) ;

suppose A1: k in dom ((a,b) In_Power n) ; :: thesis: not ((a,b) In_Power n) . k is negative

then k >= 1 by FINSEQ_3:25;
then reconsider l = k - 1 as Nat ;
len ((a,b) In_Power n) >= l + 1 by FINSEQ_3:25, A1;
then n + 1 >= l + 1 by NEWTON:def 4;
then reconsider m = n - l as Element of NAT by XREAL_1:6, NAT_1:21;
((a,b) In_Power n) . k = ((n choose l) * (a |^ m)) * (b |^ l) by A1, NEWTON:def 4;
hence not ((a,b) In_Power n) . k is negative ; :: thesis: verum

end;

suppose not k in dom ((a,b) In_Power n) ; :: thesis: not ((a,b) In_Power n) . k is negative

hence not ((a,b) In_Power n) . k is negative by FUNCT_1:def 2; :: thesis: verum

end;

end;