let i, n be Nat; :: thesis: for a, b being Integer holds a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)
let a, b be Integer; :: thesis: a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)

per cases ( i in dom ((a,b) In_Power ((n + 1) - 1)) or not i in dom ((a,b) In_Power ((n + 1) - 1)) ) ;

suppose A1: i in dom ((a,b) In_Power ((n + 1) - 1)) ; :: thesis: a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)

then A1a: i in dom ((a,b) Subnomial ((n + 1) - 1)) by DOMN;
then A1b: ( 1 <= i & i <= len ((a,b) Subnomial ((n + 1) - 1)) ) by FINSEQ_3:25;
then A1c: ( 1 - 1 <= i - 1 & i - 1 <= n ) by XREAL_1:9;
reconsider m = i - 1 as Nat by A1b;
n - m >= m - m by A1c, XREAL_1:9;
then reconsider l = n - m as Nat by INT_1:3;
A2: ((a,b) In_Power n) . i = ((n choose m) * (a |^ l)) * (b |^ m) by A1, NEWTON:def 4;
A3: (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i) = (((n choose m) * (a |^ l)) * (b |^ m)) - ((a |^ l) * (b |^ m)) by A1a, Def2, A2
.= ((n choose m) - 1) * ((a |^ l) * (b |^ m)) ;

per cases ( m = 0 or m = n or ( m > 0 & m <> n ) ) ;

suppose ( m = 0 or m = n ) ; :: thesis: a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)

then n choose m = 1 by NEWTON:19, NEWTON:21;
hence a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i) by A3, INT_2:12; :: thesis: verum

end;

suppose ( m > 0 & m <> n ) ; :: thesis: a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)

then ( 0 < m & m < n ) by A1c, XXREAL_0:1;
then ( m > 0 & n - m > m - m ) by XREAL_1:9;
then ( a divides a |^ l & b divides b |^ m ) by NEWTON02:14;
then a * b divides (a |^ l) * (b |^ m) by NEWTON02:2;
hence a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i) by A3, INT_2:2; :: thesis: verum

end;

end;

end;

suppose A1: not i in dom ((a,b) In_Power ((n + 1) - 1)) ; :: thesis: a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i)

then not i in dom ((a,b) Subnomial ((n + 1) - 1)) by DOMN;
then ( ((a,b) In_Power n) . i = 0 & ((a,b) Subnomial n) . i = 0 ) by A1, FUNCT_1:def 2;
hence a * b divides (((a,b) In_Power n) . i) - (((a,b) Subnomial n) . i) by INT_2:12; :: thesis: verum

end;

end;