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