deffunc H₁( Element of n -tuples_on BOOLEAN, Element of n -tuples_on BOOLEAN) -> Element of n -tuples_on BOOLEAN = Op-XOR ($1,$2);
consider f being Function of [:(n -tuples_on BOOLEAN),(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) such that
A1: for x, y being Element of n -tuples_on BOOLEAN holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
take f ; :: thesis: for x, y being Element of n -tuples_on BOOLEAN holds f . (x,y) = Op-XOR (x,y)
thus for x, y being Element of n -tuples_on BOOLEAN holds f . (x,y) = Op-XOR (x,y) by A1; :: thesis: verum