thus ( DES-PIP is one-to-one & DES-PIP is onto ) by THIPP1, FUNCT_2:23, THIPP2; :: according to FUNCT_2:def 4 :: thesis: verum