let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,(PI / 2).] implies integral (cos,A) = 1 )
assume A = [.0,(PI / 2).] ; :: thesis: integral (cos,A) = 1
then ( upper_bound A = PI / 2 & lower_bound A = 0 ) by Th37;
then integral (cos,A) = 1 - (sin . 0) by Th39, SIN_COS:77
.= 1 - (cos . ((PI / 2) - 0)) by SIN_COS:78
.= 1 - 0 by SIN_COS:77 ;
hence integral (cos,A) = 1 ; :: thesis: verum