let A be 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 ( 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:56; :: thesis: verum