let m, n be Nat; :: thesis: ( m in dom (((Newton_Coeff n) | n) /^ 1) implies (((Newton_Coeff n) | n) /^ 1) . m = (Newton_Coeff n) . (m + 1) )

A1: ( n = 0 implies (Newton_Coeff n) | n = {} ) ;

( n > 0 implies n in dom (Newton_Coeff n) ) by Th30;

hence ( m in dom (((Newton_Coeff n) | n) /^ 1) implies (((Newton_Coeff n) | n) /^ 1) . m = (Newton_Coeff n) . (m + 1) ) by A1, Th29; :: thesis: verum

A1: ( n = 0 implies (Newton_Coeff n) | n = {} ) ;

( n > 0 implies n in dom (Newton_Coeff n) ) by Th30;

hence ( m in dom (((Newton_Coeff n) | n) /^ 1) implies (((Newton_Coeff n) | n) /^ 1) . m = (Newton_Coeff n) . (m + 1) ) by A1, Th29; :: thesis: verum