deffunc H₁( set ) -> Element of BOOLEAN = FALSE ;
thus for f1, f2 being Function of Y,BOOLEAN st ( for x being Element of Y holds f1 . x = H₁(x) ) & ( for x being Element of Y holds f2 . x = H₁(x) ) holds
f1 = f2 from BVFUNC_1:sch 1(); :: thesis: verum