let n, k be Element of NAT ; :: thesis: (n ! ) * (eseq . k) = (n ! ) / (k ! )
thus (n ! ) * (eseq . k) = (n ! ) * (1 / (k ! )) by Def5
.= (n ! ) / (k ! ) ; :: thesis: verum