:: Series of Positive Real Numbers. Measure Theory :: by J\'ozef Bia{\l}as :: :: Received September 27, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users
uniqueness
for b1, b2 being Function of X,(Y + Z) st ( for x being Element of X holds b1. x =(F . x)+(G . x) ) & ( for x being Element of X holds b2. x =(F . x)+(G . x) ) holds b1= b2
:: sup F and inf F for Function of X,ExtREAL
::