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 (arcsin `| ].(- 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 (arcsin `| ].(- 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 (arcsin `| ].(- 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) = (arcsin . ((sqrt 2) / 2)) - (arcsin . (- ((sqrt 2) / 2))) by A1, A2, Th9, Th62
.= (arcsin ((sqrt 2) / 2)) - (arcsin . (- ((sqrt 2) / 2))) by SIN_COS6:def 2
.= (arcsin ((sqrt 2) / 2)) - (arcsin (- ((sqrt 2) / 2))) by SIN_COS6:def 2
.= (2 * PI) / 4 by Th10, Th11 ;
hence integral (f2,A) = PI / 2 ; :: thesis: verum