let n be Nat; :: thesis: Newton_Coeff (n + 1) = (<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)
reconsider f = <*0*> ^ (Newton_Coeff n) as FinSequence of COMPLEX by NEWTON02:103;
reconsider g = (Newton_Coeff n) ^ <*0*> as FinSequence of COMPLEX by NEWTON02:103;
A1: ( len (Newton_Coeff (n + 1)) = n + 2 & n + 2 = len ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) ) by CARD_1:def 7;
for i being Nat st 1 <= i & i <= len (Newton_Coeff (n + 1)) holds
(Newton_Coeff (n + 1)) . i = ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (Newton_Coeff (n + 1)) implies (Newton_Coeff (n + 1)) . i = ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) . i )
assume B1: ( 1 <= i & i <= len (Newton_Coeff (n + 1)) ) ; :: thesis: (Newton_Coeff (n + 1)) . i = ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) . i
reconsider j = i - 1 as Nat by B1;
B2: ( 1 <= i & i <= (n + 1) + 1 ) by B1, CARD_1:def 7;
then i in Seg ((n + 1) + 1) ;
then B3: ( i in dom (Newton_Coeff (n + 1)) & i in dom ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) ) by A1, FINSEQ_1:def 3;

per cases ( i = 1 or ( 1 < i & i < (n + 1) + 1 ) or i = n + 2 ) by B2, XXREAL_0:1;

suppose i = 1 ; :: thesis: (Newton_Coeff (n + 1)) . i = ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) . i

then reconsider j = j as zero Nat ;
C2: (<*0*> ^ (Newton_Coeff n)) . (j + 1) = 0 ;
1 + 0 <= 1 + n by XREAL_1:6;
then 1 in Seg (len (Newton_Coeff ((n + 1) - 1))) ;
then 1 in dom (Newton_Coeff n) by FINSEQ_1:def 3;
then ((Newton_Coeff n) ^ <*0*>) . (j + 1) = (Newton_Coeff n) . (j + 1) by FINSEQ_1:def 7
.= 1 ;
hence (Newton_Coeff (n + 1)) . i = ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) . i by B3, C2, VALUED_1:def 1; :: thesis: verum

end;

suppose C0: ( 1 < i & i < (n + 1) + 1 ) ; :: thesis: (Newton_Coeff (n + 1)) . i = ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) . i

then C1: ( 1 + 1 <= j + 1 & j + 1 <= (n + 1) + 1 ) by INT_1:7;
reconsider j = j as non zero Nat by C0;
( 1 <= j & j <= len (Newton_Coeff ((n + 1) - 1)) ) by C1, XREAL_1:6;
then j in dom (Newton_Coeff n) by FINSEQ_3:25;
then C3: (Newton_Coeff n) . j = n choose (j - 1) by NEWTON:def 5;
( 1 <= j + 1 & j + 1 <= len (Newton_Coeff ((n + 1) - 1)) ) by C0, INT_1:7;
then C4: j + 1 in dom (Newton_Coeff n) by FINSEQ_3:25;
( (<*0*> ^ (Newton_Coeff n)) . (j + 1) = (Newton_Coeff n) . j & ((Newton_Coeff n) ^ <*0*>) . (j + 1) = (Newton_Coeff n) . (j + 1) ) by CF, FINSEQ1D7;
then (f . (j + 1)) + (g . (j + 1)) = (n choose (j - 1)) + (n choose ((j + 1) - 1)) by C3, NEWTON:def 5, C4
.= (n + 1) choose ((j - 1) + 1) by NEWTON:22
.= (Newton_Coeff (n + 1)) . (j + 1) by B3, NEWTON:def 5 ;
hence (Newton_Coeff (n + 1)) . i = ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) . i by VALUED_1:def 1, B3; :: thesis: verum

end;

suppose C1: i = n + 2 ; :: thesis: (Newton_Coeff (n + 1)) . i = ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) . i

then j = n + 1 ;
then reconsider j = j as non zero Nat ;
C3: (<*0*> ^ (Newton_Coeff n)) . (1 + j) = (Newton_Coeff n) . (n + 1) by C1, CF
.= 1 ;
(f + g) . (j + 1) = (f . (j + 1)) + (g . (j + 1)) by B3, VALUED_1:def 1
.= (Newton_Coeff (n + 1)) . ((n + 1) + 1) by C1, C3 ;
hence (Newton_Coeff (n + 1)) . i = ((<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)) . i by C1; :: thesis: verum

end;

end;

end;

hence Newton_Coeff (n + 1) = (<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>) by A1; :: thesis: verum