Definition composition_eq

Definition. composition_eq
g ∘ f = {t | ∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ f ∧ (y, z) ∈ g}