proposition: Lemma FSumx_pred' : forall n (f : forall i, i < n -> PartIR), ext_fun_seq' f -> forall x, (forall i Hi, Dom (f i Hi) x) -> Dom (FSumx n f) x.
proof: Proof. intros n f H x H0; induction n as [| n Hrecn]. simpl in |- *; auto. split. apply Hrecn. red in |- *; intros. red in H. exact (H _ _ H1 _ _ _ _ H2 X). intros; auto. apply H0. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality