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