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

end;

suppose A0:
m in dom ((a,b) In_Power n)
; :: thesis: ((a,b) In_Power n) . m is natural

then consider k being Nat such that

A1: m = 1 + k by NAT_1:10, FINSEQ_3:25;

len ((a,b) In_Power n) = n + 1 by NEWTON:def 4;

then n >= k by A0, FINSEQ_3:25, A1, XREAL_1:6;

then consider l being Nat such that

A2: n = k + l by NAT_1:10;

( k = m - 1 & l = n - k ) by A1, A2;

then ((a,b) In_Power n) . m = ((n choose k) * (a |^ l)) * (b |^ k) by A0, NEWTON:def 4;

hence ((a,b) In_Power n) . m is natural ; :: thesis: verum

end;A1: m = 1 + k by NAT_1:10, FINSEQ_3:25;

len ((a,b) In_Power n) = n + 1 by NEWTON:def 4;

then n >= k by A0, FINSEQ_3:25, A1, XREAL_1:6;

then consider l being Nat such that

A2: n = k + l by NAT_1:10;

( k = m - 1 & l = n - k ) by A1, A2;

then ((a,b) In_Power n) . m = ((n choose k) * (a |^ l)) * (b |^ k) by A0, NEWTON:def 4;

hence ((a,b) In_Power n) . m is natural ; :: thesis: verum