let A be closed-interval Subset of REAL ; :: thesis: for f, g1, g2, f2 being PartFunc of REAL ,REAL
for Z being open Subset of REAL st 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 holds
integral f,A = ((- (ln * arccot )) . (sup A)) - ((- (ln * arccot )) . (inf A))
let f, g1, g2, f2 be PartFunc of REAL ,REAL ; :: thesis: for Z being open Subset of REAL st 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 holds
integral f,A = ((- (ln * arccot )) . (sup A)) - ((- (ln * arccot )) . (inf A))
let Z be open Subset of REAL ; :: thesis: ( 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 implies integral f,A = ((- (ln * arccot )) . (sup A)) - ((- (ln * arccot )) . (inf A)) )
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: integral f,A = ((- (ln * arccot )) . (sup A)) - ((- (ln * arccot )) . (inf A))
A3: Z = (dom ((g1 + g2) ^ )) /\ ((dom f2) \ (f2 " {0 })) by A1, RFUNCT_1:def 4;
A4: ( Z c= dom ((g1 + g2) ^ ) & Z c= (dom f2) \ (f2 " {0 }) ) by A3, 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;
A5: for x being Real st x in Z holds
g1 . x = 1 by A1;
A6: (g1 + g2) ^ is_differentiable_on Z by A1, A4, A5, Th1;
A7: f2 is_differentiable_on Z by A1, SIN_COS9:82;
A8: for x being Real st x in Z holds
f2 . x <> 0 by A1;
A9: f is_differentiable_on Z by A1, A6, A7, A8, FDIFF_2:21;
A10: f | Z is continuous by FDIFF_1:33, A9;
A11: f | A is continuous by FCONT_1:17, A1, A10;
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;
A16: rng (f2 | Z) c= right_open_halfline 0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f2 | Z) or x in right_open_halfline 0 )
assume x in rng (f2 | Z) ; :: thesis: x in right_open_halfline 0
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: verum

end;

A21: f2 .: Z c= dom ln by RELAT_1:148, A16, TAYLOR_1:18;
A22: Z c= dom (ln * arccot ) by A1, A13, A21, 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;
A25: Z c= dom (- (ln * arccot )) by A22, VALUED_1:8;
A26: - (ln * arccot ) is_differentiable_on Z by A24, A25, FDIFF_1:28, X;
A27: 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: ( x in Z implies ((- (ln * arccot )) `| Z) . x = 1 / ((1 + (x ^2 )) * (arccot . x)) )
assume A28: x in Z ; :: thesis: ((- (ln * arccot )) `| Z) . x = 1 / ((1 + (x ^2 )) * (arccot . x))
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: verum

end;

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

proof

let x be Real; :: thesis: ( x in Z implies f . x = 1 / ((1 + (x ^2 )) * (arccot . x)) )
assume B2: x in Z ; :: thesis: f . x = 1 / ((1 + (x ^2 )) * (arccot . x))
(((g1 + g2) ^ ) / f2) . x = (((g1 + g2) ^ ) . x) / (f2 . x) by RFUNCT_1:def 4, B2, 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: verum

end;

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

proof

let x be Real; :: thesis: ( x in dom ((- (ln * arccot )) `| Z) implies ((- (ln * arccot )) `| Z) . x = f . x )
assume x in dom ((- (ln * arccot )) `| Z) ; :: thesis: ((- (ln * arccot )) `| Z) . x = f . x
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: verum

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 )) . (sup A)) - ((- (ln * arccot )) . (inf A)) by A1, A23, A26, INTEGRA5:13; :: thesis: verum