:: deftheorem defines DES-FFUNC DESCIP_1:def 24 :
for b₁ being Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN) holds
( b₁ = DES-FFUNC iff for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds b₁ . z = DES-F ((z `1),(z `2)) );