:: deftheorem Def17 defines DES-PIPINV DESCIP_1:def 17 :
for b₁ being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) holds
( b₁ = DES-PIPINV iff for i being Element of 64 -tuples_on BOOLEAN holds b₁ . i = DES-IPINV i );