deffunc H₁( Subset of Y) -> Element of bool X = f " $1;
thus for T1, T2 being Function of (bool Y),(bool X) st ( for y being Subset of Y holds T1 . y = H₁(y) ) & ( for y being Subset of Y holds T2 . y = H₁(y) ) holds
T1 = T2 from BINOP_2:sch 1(); :: thesis: verum