:: deftheorem Def15 defines DES-PIP DESCIP_1:def 15 :
for b₁ being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) holds
( b₁ = DES-PIP iff for i being Element of 64 -tuples_on BOOLEAN holds b₁ . i = DES-IP i );