theorem Th62: :: INTEGRA8:62

for f2 being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL st A c= ].(- 1),1.[ & 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) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A))