deffunc H₁( Element of 64 -tuples_on BOOLEAN) -> Element of 64 -tuples_on BOOLEAN = DES-IPINV $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-IPINV i
thus for i being Element of 64 -tuples_on BOOLEAN holds f . i = DES-IPINV i by P2; :: thesis: verum