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