deffunc H₁( Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = $1 'xor' ('not' $2);
thus for t1, t2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds t1 . <*x,y*> = H₁(x,y) ) & ( for x, y being Element of BOOLEAN holds t2 . <*x,y*> = H₁(x,y) ) holds
t1 = t2 from FACIRC_1:sch 2(); :: thesis: verum