fact: Definition Integral {IS : IntegrationSpace} {f : PartialFunction (X (ElemFunc IS))} (fInt : IntegrableFunction f) := IntegralSeries (let (i,_) := fInt in i).
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase