fact: Definition seqcontinuous' (A B : CPsMetricSpace) (f : CSetoid_fun A B) : CProp := forall (seq : nat -> A) (lim : A), MSseqLimit' seq lim -> MSseqLimit' (fun m : nat => f (seq m)) (f lim).
imports: CoRN.metrics.CPseudoMSpaces