theorem Th31: :: INTEGR24:31

for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b holds
for r being Real holds
( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) )