fact: Definition uc_compose_uc0 X Y Z (f:Y-->Z) : (X-->Y) --> X --> Z := Build_UniformlyContinuousFunction (is_uc_uc_compose0 f).
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List