proposition: Lemma FLim_unique_IR : forall F G HF HG, conv_fun_seq'_IR J f F contf HF -> conv_fun_seq'_IR J f G contf HG -> Feq J F G.
proof: Proof. intros F G HF HG H H0. apply included_Feq'. intros a b Hab H1. apply FLim_unique with f (fun n : nat => included_imp_Continuous _ _ (contf n) _ _ _ H1) (included_imp_Continuous _ _ HF _ _ _ H1) (included_imp_Continuous _ _ HG _ _ _ H1); auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions