proposition: Lemma FLim_unique : forall F G HF HG, conv_fun_seq' a b Hab f F contf HF -> conv_fun_seq' a b Hab f G contf HG -> Feq (Compact Hab) F G.
proof: Proof. intros F G HF HG H H0. cut (Cauchy_fun_seq _ _ Hab _ contf). intro H1. apply Feq_transitive with (Cauchy_fun_seq_Lim _ _ _ _ _ H1). FEQ. simpl in |- *. apply Limits_unique. simpl in |- *. eapply fun_conv_imp_seq_conv with (Hab := Hab) (Hxf := fun n : nat => contin_imp_inc _ _ Hab _ (contf n) x Hx'); auto. apply H. apply Feq_symmetric. FEQ. simpl in |- *. apply Limits_unique. simpl in |- *. eapply fun_conv_imp_seq_conv with (Hab := Hab) (Hxf := fun n : nat => contin_imp_inc _ _ Hab _ (contf n) x Hx'); auto. apply H0. apply conv_Cauchy_fun_seq' with F HF; auto. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval