proposition: Lemma fun_series_inc_IR : forall x, J x -> forall n, Dom (f n) x.
proof: Proof. intros x H0 n. elim (H _ _ (leEq_reflexive _ x) (compact_single_iprop J x H0)). intros contF CauchyF. apply (contin_imp_inc _ _ _ _ (contF n)). apply compact_single_prop. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions