We will prove ∀X d A : set, metric_restrict X d A = graph (setprod A A) (λp : set ⇒ apply_fun d p).

Let X, d and A be given.

Use reflexivity.

∎