deffunc H₁( Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):]) -> Element of 32 -tuples_on BOOLEAN = DES-F (($1 `1),($1 `2));
A1: for x being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds H₁(x) is Element of 32 -tuples_on BOOLEAN ;
consider f being Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN) such that
A2: for x being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds f . x = H₁(x) from FUNCT_2:sch 9(A1);
take f ; :: thesis: for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds f . z = DES-F ((z `1),(z `2))
thus for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds f . z = DES-F ((z `1),(z `2)) by A2; :: thesis: verum