theorem :: INTEGRA8:64

for f2 being PartFunc of REAL,REAL
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