let A be non empty closed_interval Subset of REAL; :: thesis:
let f, f2, g1, g2 be PartFunc of REAL,REAL; :: thesis:
let Z be open Subset of REAL; :: thesis:
assume A1: ( A c= Z & f = ((g1 + g2) ^) / f2 & f2 = arccot & Z c= ].(- 1),1.[ & g2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = 1 / ((1 + (x ^2)) * (arccot . x)) & g1 . x = 1 & f2 . x > 0 ) ) & Z = dom f ) ; :: thesis:
then Z = (dom ((g1 + g2) ^)) /\ ((dom f2) \ (f2 " {0})) by RFUNCT_1:def 1;
then A2: ( Z c= dom ((g1 + g2) ^) & Z c= (dom f2) \ (f2 " {0}) ) by XBOOLE_1:18;
for x being Real st x in Z holds
g1 . x = 1 by A1;
then A3: (g1 + g2) ^ is_differentiable_on Z by A1, A2, Th1;
A4: f2 is_differentiable_on Z by A1, SIN_COS9:82;
for x being Real st x in Z holds
f2 . x <> 0 by A1;
then f is_differentiable_on Z by A1, A3, A4, FDIFF_2:21;
then f | Z is continuous by FDIFF_1:25;
then A5: f | A is continuous by A1, FCONT_1:16;
A6: Z c= dom (f2 ^) by A2, RFUNCT_1:def 2;
dom (f2 ^) c= dom f2 by RFUNCT_1:1;
then A7: Z c= dom f2 by A6;
A8: for x being Real st x in Z holds
f2 . x > 0 by A1;
rng (f2 | Z) c= right_open_halfline 0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (f2 | Z) ; :: thesis:
then consider y being object such that
A9: ( y in dom (f2 | Z) & x = (f2 | Z) . y ) by FUNCT_1:def 3;
y in Z by A9;
then f2 . y > 0 by A1;
then (f2 | Z) . y > 0 by A9, FUNCT_1:47;
hence x in right_open_halfline 0 by A9, XXREAL_1:235; :: thesis:

end;

then f2 .: Z c= dom ln by RELAT_1:115, TAYLOR_1:18;
then A10: Z c= dom (ln * arccot) by A1, A7, FUNCT_1:101;
A11: ( f is_integrable_on A & f | A is bounded ) by A1, A5, INTEGRA5:10, INTEGRA5:11;
A12: ln * arccot is_differentiable_on Z by A1, A10, A8, SIN_COS9:90;
Z c= dom (- (ln * arccot)) by A10, VALUED_1:8;
then A13: - (ln * arccot) is_differentiable_on Z by A12, FDIFF_1:20;
A14: for x being Real st x in Z holds
((- (ln * arccot)) `| Z) . x = 1 / ((1 + (x ^2)) * (arccot . x))

proof

let x be Real; :: thesis:
assume A15: x in Z ; :: thesis:
then A16: ( - 1 < x & x < 1 ) by A1, XXREAL_1:4;
arccot is_differentiable_on Z by A1, SIN_COS9:82;
then A17: arccot is_differentiable_in x by A15, FDIFF_1:9;
A18: arccot . x > 0 by A1, A15;
A19: ln * arccot is_differentiable_in x by A12, A15, FDIFF_1:9;
((- (ln * arccot)) `| Z) . x = diff ((- (ln * arccot)),x) by A13, A15, FDIFF_1:def 7
.= (- 1) * (diff ((ln * arccot),x)) by A19, FDIFF_1:15
.= (- 1) * ((diff (arccot,x)) / (arccot . x)) by A17, A18, TAYLOR_1:20
.= (- 1) * ((- (1 / (1 + (x ^2)))) / (arccot . x)) by A16, SIN_COS9:76
.= (1 / (1 + (x ^2))) / (arccot . x)
.= 1 / ((1 + (x ^2)) * (arccot . x)) by XCMPLX_1:78 ;
hence ((- (ln * arccot)) `| Z) . x = 1 / ((1 + (x ^2)) * (arccot . x)) ; :: thesis:

end;

A20: for x being Element of REAL st x in dom ((- (ln * arccot)) `| Z) holds
((- (ln * arccot)) `| Z) . x = f . x

proof

let x be Element of REAL ; :: thesis:
assume x in dom ((- (ln * arccot)) `| Z) ; :: thesis:
then A21: x in Z by A13, FDIFF_1:def 7;
then ((- (ln * arccot)) `| Z) . x = 1 / ((1 + (x ^2)) * (arccot . x)) by A14
.= f . x by A1, A21 ;
hence ((- (ln * arccot)) `| Z) . x = f . x ; :: thesis:

end;

dom ((- (ln * arccot)) `| Z) = dom f by A1, A13, FDIFF_1:def 7;
then (- (ln * arccot)) `| Z = f by A20, PARTFUN1:5;
hence integral (f,A) = ((- (ln * arccot)) . (upper_bound A)) - ((- (ln * arccot)) . (lower_bound A)) by A1, A11, A13, INTEGRA5:13; :: thesis: