id D is BinominativeFunction of D ;
hence PPid D is BinominativeFunction of D ; :: thesis: verum