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