per cases ( m in dom ((a,b) In_Power n) or not m in dom ((a,b) In_Power n) ) ;
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;
suppose not m in dom ((a,b) In_Power n) ; :: thesis: ((a,b) In_Power n) . m is natural
hence ((a,b) In_Power n) . m is natural by FUNCT_1:def 2; :: thesis: verum
end;
end;