deffunc H₁( Element of 64 -tuples_on BOOLEAN) -> Element of 64 -tuples_on BOOLEAN = DES-IP $1;
P1: for x being Element of 64 -tuples_on BOOLEAN holds H₁(x) is Element of 64 -tuples_on BOOLEAN ;
consider f being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) such that
P2: for x being Element of 64 -tuples_on BOOLEAN holds f . x = H₁(x) from FUNCT_2:sch 9(P1);
take f ; :: thesis: for i being Element of 64 -tuples_on BOOLEAN holds f . i = DES-IP i
thus for i being Element of 64 -tuples_on BOOLEAN holds f . i = DES-IP i by P2; :: thesis: verum