let n, k be non zero Nat; :: thesis: (RHartr n) . k = n * ((n - 1) choose (k - 1))

per cases ( k in dom (RHartr n) or not k in dom (RHartr n) ) ;

suppose k in dom (RHartr n) ; :: thesis: (RHartr n) . k = n * ((n - 1) choose (k - 1))

then k <= len (RHartr n) by FINSEQ_3:25;
then ( 1 <= k & k <= n ) by CARD_1:def 7, NAT_1:14;
then k in Seg (len (Newton_Coeff (n - 1))) ;
then A1: k in dom (Newton_Coeff (n - 1)) by FINSEQ_1:def 3;
then A2: k in dom (n (#) (Newton_Coeff (n - 1))) by VALUED_1:def 5;
n * ((n - 1) choose (k - 1)) = n * ((Newton_Coeff (n - 1)) . k) by A1, NEWTON:def 5
.= (n (#) (Newton_Coeff (n - 1))) . k by A2, VALUED_1:def 5 ;
hence (RHartr n) . k = n * ((n - 1) choose (k - 1)) ; :: thesis: verum

end;

suppose B1: not k in dom (RHartr n) ; :: thesis: (RHartr n) . k = n * ((n - 1) choose (k - 1))

then ( 1 > k or k > len (RHartr n) ) by FINSEQ_3:25;
then k > n by CARD_1:def 7, INT_1:74;
then k - 1 > n - 1 by XREAL_1:9;
then n * ((n - 1) choose (k - 1)) = n * 0 by NEWTON:def 3
.= (RHartr n) . k by B1, FUNCT_1:def 2 ;
hence (RHartr n) . k = n * ((n - 1) choose (k - 1)) ; :: thesis: verum

end;

end;