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