deffunc H₁( Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):]) -> Element of 32 -tuples_on BOOLEAN = DES-F (($1 `1),($1 `2));
P1: 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
P2: for x being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds f . x = H₁(x) from FUNCT_2:sch 9(P1);
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 P2; :: thesis: verum