theorem :: COMPUT_1:27

for X being set holds {} in HFuncs X