Axiom. substitution
function f → set (dom f) → set (rng f)