:: deftheorem defines infty_ext_integral INTEGR10:def 10 :
for f being PartFunc of REAL,REAL holds infty_ext_integral f = (infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0));