let f2 be PartFunc of REAL,REAL; :: thesis: for A being non empty 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 non empty 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 that
A1: A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] and
A2: ( 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)
( upper_bound A = (sqrt 2) / 2 & lower_bound A = - ((sqrt 2) / 2) ) by A1, Th37;
then integral (f2,A) = (arccos . ((sqrt 2) / 2)) - (arccos . (- ((sqrt 2) / 2))) by A1, A2, 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