let A be closed-interval Subset of REAL; :: thesis:
let f, g1, g2, f2 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 4;
then A4: ( 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:11;
then AB: Z c= dom (g1 + g2) by A4, XBOOLE_1:1;
for x being Real st x in Z holds
g1 . x = 1 by A1;
then A6: (g1 + g2) ^ is_differentiable_on Z by A1, A4, Th1;
A7: 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, A6, A7, FDIFF_2:21;
then f | Z is continuous by FDIFF_1:33;
then A11: f | A is continuous by FCONT_1:17, A1;
A12: Z c= dom (f2 ^) by A4, RFUNCT_1:def 8;
dom (f2 ^) c= dom f2 by RFUNCT_1:11;
then A13: Z c= dom f2 by A12, XBOOLE_1:1;
A14: 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 set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (f2 | Z) ; :: thesis:
then consider y being set such that
A18: ( y in dom (f2 | Z) & x = (f2 | Z) . y ) by FUNCT_1:def 5;
y in Z by A18, RELAT_1:86;
then f2 . y > 0 by A1;
then (f2 | Z) . y > 0 by A18, FUNCT_1:70;
hence x in right_open_halfline 0 by A18, XXREAL_1:235; :: thesis:

end;

then f2 .: Z c= dom ln by RELAT_1:148, TAYLOR_1:18;
then A22: Z c= dom (ln * arccot) by A1, A13, FUNCT_1:171;
A23: ( f is_integrable_on A & f | A is bounded ) by A1, A11, INTEGRA5:10, INTEGRA5:11;
A24: ln * arccot is_differentiable_on Z by A1, A22, A14, SIN_COS9:90;
Z c= dom (- (ln * arccot)) by A22, VALUED_1:8;
then A26: - (ln * arccot) is_differentiable_on Z by A24, FDIFF_1:28, X;
A27: 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 A28: x in Z ; :: thesis:
then A29: ( - 1 < x & x < 1 ) by A1, XXREAL_1:4;
arccot is_differentiable_on Z by SIN_COS9:82, A1;
then A30: arccot is_differentiable_in x by A28, FDIFF_1:16;
A31: arccot . x > 0 by A1, A28;
A32: ln * arccot is_differentiable_in x by A24, A28, FDIFF_1:16;
((- (ln * arccot)) `| Z) . x = diff ((- (ln * arccot)),x) by A26, A28, FDIFF_1:def 8
.= (- 1) * (diff ((ln * arccot),x)) by A32, FDIFF_1:23, X
.= (- 1) * ((diff (arccot,x)) / (arccot . x)) by A30, A31, TAYLOR_1:20
.= (- 1) * ((- (1 / (1 + (x ^2)))) / (arccot . x)) by A29, SIN_COS9:76
.= (1 / (1 + (x ^2))) / (arccot . x)
.= 1 / ((1 + (x ^2)) * (arccot . x)) by XCMPLX_1:79 ;
hence ((- (ln * arccot)) `| Z) . x = 1 / ((1 + (x ^2)) * (arccot . x)) ; :: thesis:

end;

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

let x be Real; :: thesis:
assume B2: x in Z ; :: thesis:
then (((g1 + g2) ^) / f2) . x = (((g1 + g2) ^) . x) / (f2 . x) by RFUNCT_1:def 4, A1
.= (((g1 + g2) . x) ") / (f2 . x) by RFUNCT_1:def 8, A4, B2
.= (((g1 . x) + (g2 . x)) ") / (f2 . x) by VALUED_1:def 1, AB, B2
.= 1 / (((g1 . x) + (g2 . x)) * (f2 . x)) by XCMPLX_1:223
.= 1 / ((1 + ((#Z 2) . x)) * (f2 . x)) by A1, B2
.= 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;

A33: for x being Real st x in dom ((- (ln * arccot)) `| Z) holds
((- (ln * arccot)) `| Z) . x = f . x

let x be Real; :: thesis:
assume x in dom ((- (ln * arccot)) `| Z) ; :: thesis:
then A34: x in Z by A26, FDIFF_1:def 8;
then ((- (ln * arccot)) `| Z) . x = 1 / ((1 + (x ^2)) * (arccot . x)) by A27
.= f . x by B1, A34 ;
hence ((- (ln * arccot)) `| Z) . x = f . x ; :: thesis:

end;

dom ((- (ln * arccot)) `| Z) = dom f by A1, A26, FDIFF_1:def 8;
then (- (ln * arccot)) `| Z = f by A33, PARTFUN1:34;
hence integral (f,A) = ((- (ln * arccot)) . (upper_bound A)) - ((- (ln * arccot)) . (lower_bound A)) by A1, A23, A26, INTEGRA5:13; :: thesis: