proposition: Lemma continuous'_imp_seqcontinuous' : forall (A B : CPsMetricSpace) (f : CSetoid_fun A B), continuous' f -> seqcontinuous' f.
proof: Proof. intros A B f. unfold continuous' in |- *. intro H. unfold seqcontinuous' in |- *. intros seq lim. unfold MSseqLimit' in |- *. intro H0. intro n. elim H with lim n. intros p H1. elim H0 with p. intros q H2. exists q. intro m. intro H3. astepl (f lim[-d]f (seq m)). apply H1. astepl (seq m[-d]lim). apply H2. exact H3. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.CPseudoMSpaces