let f2 be PartFunc of REAL ,REAL ; :: thesis: for A being closed-interval Subset of REAL st A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds
( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2 )))) ) ) & f2 | A is continuous holds
integral f2,A = - (PI / 2)
let A be closed-interval Subset of REAL ; :: thesis: ( A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds
( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2 )))) ) ) & f2 | A is continuous implies integral f2,A = - (PI / 2) )
assume A1: ( A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds
( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2 )))) ) ) & f2 | A is continuous ) ; :: thesis: integral f2,A = - (PI / 2)
then ( upper_bound A = (sqrt 2) / 2 & lower_bound A = - ((sqrt 2) / 2) ) by Th37;
then integral f2,A = (arccos . ((sqrt 2) / 2)) - (arccos . (- ((sqrt 2) / 2))) by A1, Th9, Th63
.= (arccos ((sqrt 2) / 2)) - (arccos . (- ((sqrt 2) / 2))) by SIN_COS6:def 4
.= (arccos ((sqrt 2) / 2)) - (arccos (- ((sqrt 2) / 2))) by SIN_COS6:def 4
.= (- (2 * PI )) / 4 by Th15, Th16 ;
hence integral f2,A = - (PI / 2) ; :: thesis: verum