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 (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 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 A1: ( 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 ) ; :: 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 = (arcsin . ((sqrt 2) / 2)) - (arcsin . (- ((sqrt 2) / 2))) by A1, 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