let f2 be 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))
let A be non empty closed_interval Subset of REAL; ( 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 implies integral (f2,A) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A)) )
assume that
A1:
A c= ].(- 1),1.[
and
A2:
dom (arcsin `| ].(- 1),1.[) = dom f2
and
A3:
for x being Real holds
( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) )
and
A4:
f2 | A is continuous
; integral (f2,A) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A))
for x being Element of REAL st x in dom (arcsin `| ].(- 1),1.[) holds
(arcsin `| ].(- 1),1.[) . x = f2 . x
proof
let x be
Element of
REAL ;
( x in dom (arcsin `| ].(- 1),1.[) implies (arcsin `| ].(- 1),1.[) . x = f2 . x )
assume A5:
x in dom (arcsin `| ].(- 1),1.[)
;
(arcsin `| ].(- 1),1.[) . x = f2 . x
then A6:
(
- 1
< x &
x < 1 )
by Lm18, XXREAL_1:4;
(arcsin `| ].(- 1),1.[) . x =
diff (
arcsin,
x)
by A5, Lm18, FDIFF_1:def 7, SIN_COS6:83
.=
1
/ (sqrt (1 - (x ^2)))
by A6, SIN_COS6:83
.=
f2 . x
by A3
;
hence
(arcsin `| ].(- 1),1.[) . x = f2 . x
;
verum
end;
then A7:
arcsin `| ].(- 1),1.[ = f2
by A2, PARTFUN1:5;
( A c= dom f2 & f2 is_integrable_on A )
by A1, A2, A4, Lm18, INTEGRA5:11;
hence
integral (f2,A) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A))
by A1, A4, A7, INTEGRA5:10, INTEGRA5:13, SIN_COS6:83; verum