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
( 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;
dom ((g1 + g2) ^) c= dom (g1 + g2) by RFUNCT_1:1;
then A3: Z c= dom (g1 + g2) by A2;
for x being Real st x in Z holds
g1 . x = 1 by A1;
then A4: (g1 + g2) ^ is_differentiable_on Z by A1, A2, Th1;
A5: 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, A4, A5, FDIFF_2:21;
then f | Z is continuous by FDIFF_1:25;
then A6: f | A is continuous by A1, FCONT_1:16;
A7: Z c= dom (f2 ^) by A2, RFUNCT_1:def 2;
dom (f2 ^) c= dom f2 by RFUNCT_1:1;
then A8: Z c= dom f2 by A7;
A9: for x being Real st x in Z holds
f2 . x > 0 by A1;
rng (f2 | Z) c= right_open_halfline 0

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

end;

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

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

A21: for x being Real st x in Z holds
f . x = 1 / ((1 + (x ^2)) * (arccot . x))

let x be Real; :: thesis:
assume A22: x in Z ; :: thesis:
then (((g1 + g2) ^) / f2) . x = (((g1 + g2) ^) . x) / (f2 . x) by A1, RFUNCT_1:def 1
.= (((g1 + g2) . x) ") / (f2 . x) by A2, A22, RFUNCT_1:def 2
.= (((g1 . x) + (g2 . x)) ") / (f2 . x) by A3, A22, VALUED_1:def 1
.= 1 / (((g1 . x) + (g2 . x)) * (f2 . x)) by XCMPLX_1:221
.= 1 / ((1 + ((#Z 2) . x)) * (f2 . x)) by A1, A22
.= 1 / ((1 + (x #Z 2)) * (f2 . x)) by TAYLOR_1:def 1
.= 1 / ((1 + (x ^2)) * (arccot . x)) by A1, FDIFF_7:1 ;
hence f . x = 1 / ((1 + (x ^2)) * (arccot . x)) by A1; :: thesis:

end;

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

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

end;

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