let n, k be non zero Nat; :: thesis: (Hartr n) . k = 1 / (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: (Hartr n) . k = 1 / (n * ((n - 1) choose (k - 1)))

then k in dom (Hartr n) by VALUED_1:def 7;
then (Hartr n) . k = ((RHartr n) . k) " by VALUED_1:def 7
.= (n * ((n - 1) choose (k - 1))) " by HAR
.= 1 / (n * ((n - 1) choose (k - 1))) by XCMPLX_1:215 ;
hence (Hartr n) . k = 1 / (n * ((n - 1) choose (k - 1))) ; :: thesis: verum

end;

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

then not k in dom (Hartr n) by VALUED_1:def 7;
then (Hartr n) . k = 1 / 0 by FUNCT_1:def 2
.= 1 / ((RHartr n) . k) by B1, FUNCT_1:def 2
.= 1 / (n * ((n - 1) choose (k - 1))) by HAR ;
hence (Hartr n) . k = 1 / (n * ((n - 1) choose (k - 1))) ; :: thesis: verum

end;

end;