let A be closed-interval Subset of REAL ; :: thesis: ( A = [.0 ,1.] implies integral sinh ,A = ((number_e - 1) ^2 ) / (2 * number_e ) )
assume A = [.0 ,1.] ; :: thesis: integral sinh ,A = ((number_e - 1) ^2 ) / (2 * number_e )
then A1: ( upper_bound A = 1 & lower_bound A = 0 ) by Th37;
A2: 2 * number_e > 0

proof

exp_R 1 > 0 by SIN_COS:60;
hence 2 * number_e > 0 by IRRAT_1:def 7, XREAL_1:131; :: thesis: verum

end;

integral sinh ,A = (((number_e ^2 ) + 1) / (2 * number_e )) - 1 by A1, Th18, Th19, Th55
.= (((number_e ^2 ) + 1) / (2 * number_e )) - ((2 * number_e ) / (2 * number_e )) by A2, XCMPLX_1:60
.= (((number_e ^2 ) + 1) - (2 * number_e )) / (2 * number_e ) by XCMPLX_1:121
.= (((number_e ^2 ) - ((2 * number_e ) * 1)) + (1 ^2 )) / (2 * number_e )
.= ((number_e - 1) ^2 ) / (2 * number_e ) ;
hence integral sinh ,A = ((number_e - 1) ^2 ) / (2 * number_e ) ; :: thesis: verum