let f2 be PartFunc of REAL,REAL; 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; ( 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 )
; 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)
; verum