continuity of extension to completion

Stream: Is there code for X?

[Adam Topaz]

I'm quite sure the following is true:

import topology.uniform_space.abstract_completion

variables
  (X Y : Type*) [uniform_space X] [uniform_space Y] [complete_space Y]
  (P : abstract_completion X)

example (p : P.space) :
  continuous
  (λ e : {e : X → Y | uniform_continuous e}, P.extend e.1 p) :=
sorry

Can anyone come up with a simple proof?