fact: Definition domainInfinSumWeaveL {R : ConstructiveReals} (X : Set) (fn gn : nat -> @PartialFunction R X) (x : X) (xD : Domain (XinfiniteSumAbs (weaveSequences _ fn gn)) x) : Domain (@XinfiniteSumAbs R _ fn) x.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase