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