proposition: Lemma FSum0_0 : forall P f, (forall n, included P (Dom (f n))) -> Feq P [-C-][0] (FSum0 0 f).
proof: Proof. intros P f H. FEQ. simpl in |- *. red in |- *; intros; apply (H n); auto. Qed.
imports: CoRN.reals.CSumsReals CoRN.ftc.PartFunEquality