let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,1.] implies integral (exp_R,A) = number_e - 1 )
assume A = [.0,1.] ; :: thesis: integral (exp_R,A) = number_e - 1
then A = [.0,jj.] ;
then ( upper_bound A = 1 & lower_bound A = 0 ) by Th37;
hence integral (exp_R,A) = number_e - 1 by Th53, IRRAT_1:def 7, SIN_COS:51; :: thesis: verum