let m, n be Nat; ( 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; verum