theorem :: INTEGRA9:44
for f being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL holds ||..(1 (#) f),A..|| = ||..f,A..|| by RFUNCT_1:21;