dom {} = {} ;
hence for b₁ being Function st b₁ is empty holds
b₁ is without_fixpoints ; :: thesis: verum