theorem Th63: :: INTEGRA8:63

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