let a, b be Real; for A being non empty closed_interval Subset of REAL
for f, f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a / (sqrt (1 - (((a * x) + b) ^2))) & f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 ) ) & Z c= dom (arccos * f1) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (arccos * f1)) . (upper_bound A)) - ((- (arccos * f1)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; for f, f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a / (sqrt (1 - (((a * x) + b) ^2))) & f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 ) ) & Z c= dom (arccos * f1) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (arccos * f1)) . (upper_bound A)) - ((- (arccos * f1)) . (lower_bound A))
let f, f1 be PartFunc of REAL,REAL; for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a / (sqrt (1 - (((a * x) + b) ^2))) & f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 ) ) & Z c= dom (arccos * f1) & Z = dom f & f | A is continuous holds
integral (f,A) = ((- (arccos * f1)) . (upper_bound A)) - ((- (arccos * f1)) . (lower_bound A))
let Z be open Subset of REAL; ( A c= Z & ( for x being Real st x in Z holds
( f . x = a / (sqrt (1 - (((a * x) + b) ^2))) & f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 ) ) & Z c= dom (arccos * f1) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (arccos * f1)) . (upper_bound A)) - ((- (arccos * f1)) . (lower_bound A)) )
assume A1:
( A c= Z & ( for x being Real st x in Z holds
( f . x = a / (sqrt (1 - (((a * x) + b) ^2))) & f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 ) ) & Z c= dom (arccos * f1) & Z = dom f & f | A is continuous )
; integral (f,A) = ((- (arccos * f1)) . (upper_bound A)) - ((- (arccos * f1)) . (lower_bound A))
then A2:
( f is_integrable_on A & f | A is bounded )
by INTEGRA5:10, INTEGRA5:11;
A3:
for x being Real st x in Z holds
f1 . x = (a * x) + b
by A1;
A4:
for x being Real st x in Z holds
( f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 )
by A1;
A5:
Z c= dom (- (arccos * f1))
by A1, VALUED_1:8;
A6:
arccos * f1 is_differentiable_on Z
by A1, A4, FDIFF_7:15;
then A7:
(- 1) (#) (arccos * f1) is_differentiable_on Z
by A5, FDIFF_1:20;
for y being object st y in Z holds
y in dom f1
by A1, FUNCT_1:11;
then A8:
Z c= dom f1
;
then A9:
( f1 is_differentiable_on Z & ( for x being Real st x in Z holds
(f1 `| Z) . x = a ) )
by A3, FDIFF_1:23;
A10:
for x being Real st x in Z holds
((- (arccos * f1)) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2)))
proof
let x be
Real;
( x in Z implies ((- (arccos * f1)) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2))) )
assume A11:
x in Z
;
((- (arccos * f1)) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2)))
then A12:
f1 is_differentiable_in x
by A9, FDIFF_1:9;
A13:
(
f1 . x > - 1 &
f1 . x < 1 )
by A1, A11;
A14:
arccos * f1 is_differentiable_in x
by A6, A11, FDIFF_1:9;
((- (arccos * f1)) `| Z) . x =
diff (
(- (arccos * f1)),
x)
by A7, A11, FDIFF_1:def 7
.=
(- 1) * (diff ((arccos * f1),x))
by A14, FDIFF_1:15
.=
(- 1) * (- ((diff (f1,x)) / (sqrt (1 - ((f1 . x) ^2)))))
by A12, A13, FDIFF_7:7
.=
(- 1) * (- (((f1 `| Z) . x) / (sqrt (1 - ((f1 . x) ^2)))))
by A9, A11, FDIFF_1:def 7
.=
(- 1) * (- (a / (sqrt (1 - ((f1 . x) ^2)))))
by A3, A8, A11, FDIFF_1:23
.=
a / (sqrt (1 - (((a * x) + b) ^2)))
by A1, A11
;
hence
((- (arccos * f1)) `| Z) . x = a / (sqrt (1 - (((a * x) + b) ^2)))
;
verum
end;
A15:
for x being Element of REAL st x in dom ((- (arccos * f1)) `| Z) holds
((- (arccos * f1)) `| Z) . x = f . x
dom ((- (arccos * f1)) `| Z) = dom f
by A1, A7, FDIFF_1:def 7;
then
(- (arccos * f1)) `| Z = f
by A15, PARTFUN1:5;
hence
integral (f,A) = ((- (arccos * f1)) . (upper_bound A)) - ((- (arccos * f1)) . (lower_bound A))
by A1, A2, A7, INTEGRA5:13; verum