:: INTEGR14 semantic presentation begin Lm1: for Z being open Subset of REAL st 0 in Z holds (id Z) " {0} = {0} proof let Z be open Subset of REAL; ::_thesis: ( 0 in Z implies (id Z) " {0} = {0} ) assume A1: 0 in Z ; ::_thesis: (id Z) " {0} = {0} thus (id Z) " {0} c= {0} :: according to XBOOLE_0:def_10 ::_thesis: {0} c= (id Z) " {0} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (id Z) " {0} or x in {0} ) assume A2: x in (id Z) " {0} ; ::_thesis: x in {0} then x in dom (id Z) by FUNCT_1:def_7; then A3: x in Z ; (id Z) . x in {0} by A2, FUNCT_1:def_7; hence x in {0} by A3, FUNCT_1:18; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {0} or x in (id Z) " {0} ) assume x in {0} ; ::_thesis: x in (id Z) " {0} then A4: x = 0 by TARSKI:def_1; then (id Z) . x = 0 by A1, FUNCT_1:18; then A5: (id Z) . x in {0} by TARSKI:def_1; x in dom (id Z) by A1, A4; hence x in (id Z) " {0} by A5, FUNCT_1:def_7; ::_thesis: verum end; theorem Th1: :: INTEGR14:1 for Z being open Subset of REAL st Z c= dom (sec * ((id Z) ^)) holds ( - (sec * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sec * ((id Z) ^)) implies ( - (sec * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) ) ) assume A1: Z c= dom (sec * ((id Z) ^)) ; ::_thesis: ( - (sec * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) ) then A2: Z c= dom (- (sec * ((id Z) ^))) by VALUED_1:def_5; A3: Z c= dom ((id Z) ^) by A1, FUNCT_1:101; A4: not 0 in Z proof assume A5: 0 in Z ; ::_thesis: contradiction dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2 .= (dom (id Z)) \ {0} by Lm1, A5 ; then not 0 in {0} by A5, A3, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then A6: sec * ((id Z) ^) is_differentiable_on Z by A1, FDIFF_9:8; then A7: (- 1) (#) (sec * ((id Z) ^)) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) assume A8: x in Z ; ::_thesis: ((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ((- (sec * ((id Z) ^))) `| Z) . x = ((- 1) (#) ((sec * ((id Z) ^)) `| Z)) . x by A6, FDIFF_2:19 .= (- 1) * (((sec * ((id Z) ^)) `| Z) . x) by VALUED_1:6 .= (- 1) * (- ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)))) by A1, A4, A8, FDIFF_9:8 .= (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ; hence ((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ; ::_thesis: verum end; hence ( - (sec * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) ) by A7; ::_thesis: verum end; theorem Th2: :: INTEGR14:2 for Z being open Subset of REAL st Z c= dom (cosec * exp_R) holds ( - (cosec * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * exp_R) implies ( - (cosec * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) ) ) assume A1: Z c= dom (cosec * exp_R) ; ::_thesis: ( - (cosec * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) ) then A2: Z c= dom (- (cosec * exp_R)) by VALUED_1:8; A3: cosec * exp_R is_differentiable_on Z by A1, FDIFF_9:13; then A4: (- 1) (#) (cosec * exp_R) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) assume A5: x in Z ; ::_thesis: ((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ((- (cosec * exp_R)) `| Z) . x = ((- 1) (#) ((cosec * exp_R) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * (((cosec * exp_R) `| Z) . x) by VALUED_1:6 .= (- 1) * (- (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2))) by A1, A5, FDIFF_9:13 .= ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ; hence ((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ; ::_thesis: verum end; hence ( - (cosec * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) ) by A4; ::_thesis: verum end; theorem Th3: :: INTEGR14:3 for Z being open Subset of REAL st Z c= dom (cosec * ln) holds ( - (cosec * ln) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * ln) implies ( - (cosec * ln) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) ) ) assume A1: Z c= dom (cosec * ln) ; ::_thesis: ( - (cosec * ln) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) ) then A2: Z c= dom (- (cosec * ln)) by VALUED_1:8; A3: cosec * ln is_differentiable_on Z by A1, FDIFF_9:15; then A4: (- 1) (#) (cosec * ln) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) assume A5: x in Z ; ::_thesis: ((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ((- (cosec * ln)) `| Z) . x = ((- 1) (#) ((cosec * ln) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * (((cosec * ln) `| Z) . x) by VALUED_1:6 .= (- 1) * (- ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)))) by A1, A5, FDIFF_9:15 .= (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ; hence ((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ; ::_thesis: verum end; hence ( - (cosec * ln) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) ) by A4; ::_thesis: verum end; theorem Th4: :: INTEGR14:4 for Z being open Subset of REAL st Z c= dom (exp_R * cosec) holds ( - (exp_R * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (exp_R * cosec) implies ( - (exp_R * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) ) ) assume A1: Z c= dom (exp_R * cosec) ; ::_thesis: ( - (exp_R * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) ) then A2: Z c= dom (- (exp_R * cosec)) by VALUED_1:8; A3: exp_R * cosec is_differentiable_on Z by A1, FDIFF_9:17; then A4: (- 1) (#) (exp_R * cosec) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) assume A5: x in Z ; ::_thesis: ((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ((- (exp_R * cosec)) `| Z) . x = ((- 1) (#) ((exp_R * cosec) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * (((exp_R * cosec) `| Z) . x) by VALUED_1:6 .= (- 1) * (- (((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2))) by A1, A5, FDIFF_9:17 .= ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ; hence ((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ; ::_thesis: verum end; hence ( - (exp_R * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) ) by A4; ::_thesis: verum end; theorem Th5: :: INTEGR14:5 for Z being open Subset of REAL st Z c= dom (ln * cosec) holds ( - (ln * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * cosec)) `| Z) . x = cot . x ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * cosec) implies ( - (ln * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * cosec)) `| Z) . x = cot . x ) ) ) assume A1: Z c= dom (ln * cosec) ; ::_thesis: ( - (ln * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * cosec)) `| Z) . x = cot . x ) ) then A2: Z c= dom (- (ln * cosec)) by VALUED_1:8; A3: ln * cosec is_differentiable_on Z by A1, FDIFF_9:19; then A4: (- 1) (#) (ln * cosec) is_differentiable_on Z by A2, FDIFF_1:20; A5: for x being Real st x in Z holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 ) assume x in Z ; ::_thesis: sin . x <> 0 then x in dom cosec by A1, FUNCT_1:11; hence sin . x <> 0 by RFUNCT_1:3; ::_thesis: verum end; for x being Real st x in Z holds ((- (ln * cosec)) `| Z) . x = cot . x proof let x be Real; ::_thesis: ( x in Z implies ((- (ln * cosec)) `| Z) . x = cot . x ) assume A6: x in Z ; ::_thesis: ((- (ln * cosec)) `| Z) . x = cot . x ((- (ln * cosec)) `| Z) . x = ((- 1) (#) ((ln * cosec) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * (((ln * cosec) `| Z) . x) by VALUED_1:6 .= (- 1) * (- ((cos . x) / (sin . x))) by A1, A6, FDIFF_9:19 .= cot x .= cot . x by A5, A6, SIN_COS9:16 ; hence ((- (ln * cosec)) `| Z) . x = cot . x ; ::_thesis: verum end; hence ( - (ln * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * cosec)) `| Z) . x = cot . x ) ) by A4; ::_thesis: verum end; theorem Th6: :: INTEGR14:6 for n being Nat for Z being open Subset of REAL st Z c= dom ((#Z n) * cosec) & 1 <= n holds ( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) ) proof let n be Nat; ::_thesis: for Z being open Subset of REAL st Z c= dom ((#Z n) * cosec) & 1 <= n holds ( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((#Z n) * cosec) & 1 <= n implies ( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) ) ) assume A1: ( Z c= dom ((#Z n) * cosec) & 1 <= n ) ; ::_thesis: ( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) ) then A2: ( Z c= dom (- ((#Z n) * cosec)) & 1 <= n ) by VALUED_1:8; A3: (#Z n) * cosec is_differentiable_on Z by A1, FDIFF_9:21; then A4: (- 1) (#) ((#Z n) * cosec) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) proof let x be Real; ::_thesis: ( x in Z implies ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) assume A5: x in Z ; ::_thesis: ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ((- ((#Z n) * cosec)) `| Z) . x = ((- 1) (#) (((#Z n) * cosec) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * ((((#Z n) * cosec) `| Z) . x) by VALUED_1:6 .= (- 1) * (- ((n * (cos . x)) / ((sin . x) #Z (n + 1)))) by A1, A5, FDIFF_9:21 .= (n * (cos . x)) / ((sin . x) #Z (n + 1)) ; hence ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ; ::_thesis: verum end; hence ( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) ) by A4; ::_thesis: verum end; theorem Th7: :: INTEGR14:7 for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) sec) holds ( - (((id Z) ^) (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (((id Z) ^) (#) sec) implies ( - (((id Z) ^) (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) ) ) assume A1: Z c= dom (((id Z) ^) (#) sec) ; ::_thesis: ( - (((id Z) ^) (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) ) then A2: Z c= dom (- (((id Z) ^) (#) sec)) by VALUED_1:8; Z c= (dom ((id Z) ^)) /\ (dom sec) by A1, VALUED_1:def_4; then A3: Z c= dom ((id Z) ^) by XBOOLE_1:18; A4: not 0 in Z proof assume A5: 0 in Z ; ::_thesis: contradiction dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2 .= (dom (id Z)) \ {0} by Lm1, A5 ; then not 0 in {0} by A5, A3, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then A6: ((id Z) ^) (#) sec is_differentiable_on Z by A1, FDIFF_9:32; then A7: (- 1) (#) (((id Z) ^) (#) sec) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) assume A8: x in Z ; ::_thesis: ((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ((- (((id Z) ^) (#) sec)) `| Z) . x = ((- 1) (#) ((((id Z) ^) (#) sec) `| Z)) . x by A6, FDIFF_2:19 .= (- 1) * (((((id Z) ^) (#) sec) `| Z) . x) by VALUED_1:6 .= (- 1) * ((- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2))) by A1, A4, A8, FDIFF_9:32 .= ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ; hence ((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ; ::_thesis: verum end; hence ( - (((id Z) ^) (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) ) by A7; ::_thesis: verum end; theorem Th8: :: INTEGR14:8 for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) cosec) holds ( - (((id Z) ^) (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (((id Z) ^) (#) cosec) implies ( - (((id Z) ^) (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (((id Z) ^) (#) cosec) ; ::_thesis: ( - (((id Z) ^) (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) ) then A2: Z c= dom (- (((id Z) ^) (#) cosec)) by VALUED_1:8; Z c= (dom ((id Z) ^)) /\ (dom cosec) by A1, VALUED_1:def_4; then A3: Z c= dom ((id Z) ^) by XBOOLE_1:18; A4: not 0 in Z proof assume A5: 0 in Z ; ::_thesis: contradiction dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2 .= (dom (id Z)) \ {0} by Lm1, A5 ; then not 0 in {0} by A5, A3, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then A6: ((id Z) ^) (#) cosec is_differentiable_on Z by A1, FDIFF_9:33; then A7: (- 1) (#) (((id Z) ^) (#) cosec) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) assume A8: x in Z ; ::_thesis: ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((- 1) (#) ((((id Z) ^) (#) cosec) `| Z)) . x by A6, FDIFF_2:19 .= (- 1) * (((((id Z) ^) (#) cosec) `| Z) . x) by VALUED_1:6 .= (- 1) * ((- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2))) by A1, A4, A8, FDIFF_9:33 .= ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ; hence ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( - (((id Z) ^) (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) ) by A7; ::_thesis: verum end; theorem Th9: :: INTEGR14:9 for Z being open Subset of REAL st Z c= dom (cosec * sin) holds ( - (cosec * sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * sin) implies ( - (cosec * sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) ) ) assume A1: Z c= dom (cosec * sin) ; ::_thesis: ( - (cosec * sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) ) then A2: Z c= dom (- (cosec * sin)) by VALUED_1:8; A3: cosec * sin is_differentiable_on Z by A1, FDIFF_9:36; then A4: (- 1) (#) (cosec * sin) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) assume A5: x in Z ; ::_thesis: ((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ((- (cosec * sin)) `| Z) . x = ((- 1) (#) ((cosec * sin) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * (((cosec * sin) `| Z) . x) by VALUED_1:6 .= (- 1) * (- (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2))) by A1, A5, FDIFF_9:36 .= ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ; hence ((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ; ::_thesis: verum end; hence ( - (cosec * sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) ) by A4; ::_thesis: verum end; theorem Th10: :: INTEGR14:10 for Z being open Subset of REAL st Z c= dom (sec * cot) holds ( - (sec * cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sec * cot) implies ( - (sec * cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) ) ) assume A1: Z c= dom (sec * cot) ; ::_thesis: ( - (sec * cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) ) then A2: Z c= dom (- (sec * cot)) by VALUED_1:8; A3: sec * cot is_differentiable_on Z by A1, FDIFF_9:39; then A4: (- 1) (#) (sec * cot) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) assume A5: x in Z ; ::_thesis: ((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ((- (sec * cot)) `| Z) . x = ((- 1) (#) ((sec * cot) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * (((sec * cot) `| Z) . x) by VALUED_1:6 .= (- 1) * (- (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2))) by A1, A5, FDIFF_9:39 .= ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ; hence ((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ; ::_thesis: verum end; hence ( - (sec * cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) ) by A4; ::_thesis: verum end; theorem Th11: :: INTEGR14:11 for Z being open Subset of REAL st Z c= dom (cosec * tan) holds ( - (cosec * tan) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cosec * tan) implies ( - (cosec * tan) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) ) ) assume A1: Z c= dom (cosec * tan) ; ::_thesis: ( - (cosec * tan) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) ) then A2: Z c= dom (- (cosec * tan)) by VALUED_1:8; A3: cosec * tan is_differentiable_on Z by A1, FDIFF_9:40; dom (cosec * tan) c= dom tan by RELAT_1:25; then A4: Z c= dom tan by A1, XBOOLE_1:1; A5: (- 1) (#) (cosec * tan) is_differentiable_on Z by A2, A3, FDIFF_1:20; A6: for x being Real st x in Z holds sin . (tan . x) <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . (tan . x) <> 0 ) assume x in Z ; ::_thesis: sin . (tan . x) <> 0 then tan . x in dom cosec by A1, FUNCT_1:11; hence sin . (tan . x) <> 0 by RFUNCT_1:3; ::_thesis: verum end; for x being Real st x in Z holds ((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) assume A7: x in Z ; ::_thesis: ((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) then A8: cos . x <> 0 by A4, FDIFF_8:1; then A9: tan is_differentiable_in x by FDIFF_7:46; A10: sin . (tan . x) <> 0 by A6, A7; then A11: cosec is_differentiable_in tan . x by FDIFF_9:2; A12: cosec * tan is_differentiable_in x by A3, A7, FDIFF_1:9; ((- (cosec * tan)) `| Z) . x = diff ((- (cosec * tan)),x) by A5, A7, FDIFF_1:def_7 .= (- 1) * (diff ((cosec * tan),x)) by A12, FDIFF_1:15 .= (- 1) * ((diff (cosec,(tan . x))) * (diff (tan,x))) by A9, A11, FDIFF_2:13 .= (- 1) * ((- ((cos . (tan . x)) / ((sin . (tan . x)) ^2))) * (diff (tan,x))) by A10, FDIFF_9:2 .= (- 1) * ((1 / ((cos . x) ^2)) * (- ((cos . (tan . x)) / ((sin . (tan . x)) ^2)))) by A8, FDIFF_7:46 .= ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ; hence ((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ; ::_thesis: verum end; hence ( - (cosec * tan) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) ) by A5; ::_thesis: verum end; theorem Th12: :: INTEGR14:12 for Z being open Subset of REAL st Z c= dom (cot (#) sec) holds ( - (cot (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot (#) sec) implies ( - (cot (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) ) ) assume A1: Z c= dom (cot (#) sec) ; ::_thesis: ( - (cot (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) ) then A2: Z c= dom (- (cot (#) sec)) by VALUED_1:8; A3: cot (#) sec is_differentiable_on Z by A1, FDIFF_9:43; then A4: (- 1) (#) (cot (#) sec) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) assume A5: x in Z ; ::_thesis: ((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ((- (cot (#) sec)) `| Z) . x = ((- 1) (#) ((cot (#) sec) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * (((cot (#) sec) `| Z) . x) by VALUED_1:6 .= (- 1) * ((- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2))) by A1, A5, FDIFF_9:43 .= ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ; hence ((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ; ::_thesis: verum end; hence ( - (cot (#) sec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) ) by A4; ::_thesis: verum end; theorem Th13: :: INTEGR14:13 for Z being open Subset of REAL st Z c= dom (cot (#) cosec) holds ( - (cot (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cot (#) cosec) implies ( - (cot (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (cot (#) cosec) ; ::_thesis: ( - (cot (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) ) then A2: Z c= dom (- (cot (#) cosec)) by VALUED_1:8; A3: cot (#) cosec is_differentiable_on Z by A1, FDIFF_9:45; then A4: (- 1) (#) (cot (#) cosec) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) assume A5: x in Z ; ::_thesis: ((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ((- (cot (#) cosec)) `| Z) . x = ((- 1) (#) ((cot (#) cosec) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * (((cot (#) cosec) `| Z) . x) by VALUED_1:6 .= (- 1) * ((- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2))) by A1, A5, FDIFF_9:45 .= ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ; hence ((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( - (cot (#) cosec) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) ) by A4; ::_thesis: verum end; theorem Th14: :: INTEGR14:14 for Z being open Subset of REAL st Z c= dom (cos (#) cot) holds ( - (cos (#) cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (cos (#) cot) implies ( - (cos (#) cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom (cos (#) cot) ; ::_thesis: ( - (cos (#) cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) ) then A2: Z c= dom (- (cos (#) cot)) by VALUED_1:8; A3: cos (#) cot is_differentiable_on Z by A1, FDIFF_10:11; then A4: (- 1) (#) (cos (#) cot) is_differentiable_on Z by A2, FDIFF_1:20; for x being Real st x in Z holds ((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) assume A5: x in Z ; ::_thesis: ((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ((- (cos (#) cot)) `| Z) . x = ((- 1) (#) ((cos (#) cot) `| Z)) . x by A3, FDIFF_2:19 .= (- 1) * (((cos (#) cot) `| Z) . x) by VALUED_1:6 .= (- 1) * ((- (cos . x)) - ((cos . x) / ((sin . x) ^2))) by A1, A5, FDIFF_10:11 .= (cos . x) + ((cos . x) / ((sin . x) ^2)) ; hence ((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( - (cos (#) cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) ) by A4; ::_thesis: verum end; begin theorem :: INTEGR14:15 for A being non empty closed_interval Subset of REAL for f 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 = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) & Z c= dom (sec * ((id Z) ^)) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sec * ((id Z) ^))) . (upper_bound A)) - ((- (sec * ((id Z) ^))) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) & Z c= dom (sec * ((id Z) ^)) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sec * ((id Z) ^))) . (upper_bound A)) - ((- (sec * ((id Z) ^))) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) & Z c= dom (sec * ((id Z) ^)) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sec * ((id Z) ^))) . (upper_bound A)) - ((- (sec * ((id Z) ^))) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) & Z c= dom (sec * ((id Z) ^)) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (sec * ((id Z) ^))) . (upper_bound A)) - ((- (sec * ((id Z) ^))) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) ) & Z c= dom (sec * ((id Z) ^)) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (sec * ((id Z) ^))) . (upper_bound A)) - ((- (sec * ((id Z) ^))) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (sec * ((id Z) ^)) is_differentiable_on Z by A1, Th1; A4: for x being Real st x in dom ((- (sec * ((id Z) ^))) `| Z) holds ((- (sec * ((id Z) ^))) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (sec * ((id Z) ^))) `| Z) implies ((- (sec * ((id Z) ^))) `| Z) . x = f . x ) assume x in dom ((- (sec * ((id Z) ^))) `| Z) ; ::_thesis: ((- (sec * ((id Z) ^))) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (sec * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) by A1, Th1 .= f . x by A1, A5 ; hence ((- (sec * ((id Z) ^))) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (sec * ((id Z) ^))) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (sec * ((id Z) ^))) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (sec * ((id Z) ^))) . (upper_bound A)) - ((- (sec * ((id Z) ^))) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:16 for A being non empty closed_interval Subset of REAL for f 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 = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) & Z c= dom (cosec * ((id Z) ^)) & Z = dom f & f | A is continuous holds integral (f,A) = ((cosec * ((id Z) ^)) . (upper_bound A)) - ((cosec * ((id Z) ^)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) & Z c= dom (cosec * ((id Z) ^)) & Z = dom f & f | A is continuous holds integral (f,A) = ((cosec * ((id Z) ^)) . (upper_bound A)) - ((cosec * ((id Z) ^)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) & Z c= dom (cosec * ((id Z) ^)) & Z = dom f & f | A is continuous holds integral (f,A) = ((cosec * ((id Z) ^)) . (upper_bound A)) - ((cosec * ((id Z) ^)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) & Z c= dom (cosec * ((id Z) ^)) & Z = dom f & f | A is continuous implies integral (f,A) = ((cosec * ((id Z) ^)) . (upper_bound A)) - ((cosec * ((id Z) ^)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) ) & Z c= dom (cosec * ((id Z) ^)) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((cosec * ((id Z) ^)) . (upper_bound A)) - ((cosec * ((id Z) ^)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: Z c= dom ((id Z) ^) by A1, FUNCT_1:101; A4: not 0 in Z proof assume A5: 0 in Z ; ::_thesis: contradiction dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2 .= (dom (id Z)) \ {0} by Lm1, A5 ; then not 0 in {0} by A5, A3, XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; then A6: cosec * ((id Z) ^) is_differentiable_on Z by A1, FDIFF_9:9; A7: for x being Real st x in dom ((cosec * ((id Z) ^)) `| Z) holds ((cosec * ((id Z) ^)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((cosec * ((id Z) ^)) `| Z) implies ((cosec * ((id Z) ^)) `| Z) . x = f . x ) assume x in dom ((cosec * ((id Z) ^)) `| Z) ; ::_thesis: ((cosec * ((id Z) ^)) `| Z) . x = f . x then A8: x in Z by A6, FDIFF_1:def_7; then ((cosec * ((id Z) ^)) `| Z) . x = (cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) by A1, A4, FDIFF_9:9 .= f . x by A1, A8 ; hence ((cosec * ((id Z) ^)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((cosec * ((id Z) ^)) `| Z) = dom f by A1, A6, FDIFF_1:def_7; then (cosec * ((id Z) ^)) `| Z = f by A7, PARTFUN1:5; hence integral (f,A) = ((cosec * ((id Z) ^)) . (upper_bound A)) - ((cosec * ((id Z) ^)) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:17 for A being non empty closed_interval Subset of REAL for f 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 = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) & Z c= dom (sec * exp_R) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * exp_R) . (upper_bound A)) - ((sec * exp_R) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) & Z c= dom (sec * exp_R) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * exp_R) . (upper_bound A)) - ((sec * exp_R) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) & Z c= dom (sec * exp_R) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * exp_R) . (upper_bound A)) - ((sec * exp_R) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) & Z c= dom (sec * exp_R) & Z = dom f & f | A is continuous implies integral (f,A) = ((sec * exp_R) . (upper_bound A)) - ((sec * exp_R) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) ) & Z c= dom (sec * exp_R) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((sec * exp_R) . (upper_bound A)) - ((sec * exp_R) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: sec * exp_R is_differentiable_on Z by A1, FDIFF_9:12; A4: for x being Real st x in dom ((sec * exp_R) `| Z) holds ((sec * exp_R) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((sec * exp_R) `| Z) implies ((sec * exp_R) `| Z) . x = f . x ) assume x in dom ((sec * exp_R) `| Z) ; ::_thesis: ((sec * exp_R) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((sec * exp_R) `| Z) . x = ((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) by A1, FDIFF_9:12 .= f . x by A1, A5 ; hence ((sec * exp_R) `| Z) . x = f . x ; ::_thesis: verum end; dom ((sec * exp_R) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (sec * exp_R) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((sec * exp_R) . (upper_bound A)) - ((sec * exp_R) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:18 for A being non empty closed_interval Subset of REAL for f 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 = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) & Z c= dom (cosec * exp_R) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * exp_R)) . (upper_bound A)) - ((- (cosec * exp_R)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) & Z c= dom (cosec * exp_R) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * exp_R)) . (upper_bound A)) - ((- (cosec * exp_R)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) & Z c= dom (cosec * exp_R) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * exp_R)) . (upper_bound A)) - ((- (cosec * exp_R)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) & Z c= dom (cosec * exp_R) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cosec * exp_R)) . (upper_bound A)) - ((- (cosec * exp_R)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) ) & Z c= dom (cosec * exp_R) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cosec * exp_R)) . (upper_bound A)) - ((- (cosec * exp_R)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (cosec * exp_R) is_differentiable_on Z by A1, Th2; A4: for x being Real st x in dom ((- (cosec * exp_R)) `| Z) holds ((- (cosec * exp_R)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (cosec * exp_R)) `| Z) implies ((- (cosec * exp_R)) `| Z) . x = f . x ) assume x in dom ((- (cosec * exp_R)) `| Z) ; ::_thesis: ((- (cosec * exp_R)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (cosec * exp_R)) `| Z) . x = ((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) by A1, Th2 .= f . x by A1, A5 ; hence ((- (cosec * exp_R)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (cosec * exp_R)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (cosec * exp_R)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (cosec * exp_R)) . (upper_bound A)) - ((- (cosec * exp_R)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:19 for A being non empty closed_interval Subset of REAL for f 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 = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) & Z c= dom (sec * ln) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * ln) . (upper_bound A)) - ((sec * ln) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) & Z c= dom (sec * ln) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * ln) . (upper_bound A)) - ((sec * ln) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) & Z c= dom (sec * ln) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * ln) . (upper_bound A)) - ((sec * ln) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) & Z c= dom (sec * ln) & Z = dom f & f | A is continuous implies integral (f,A) = ((sec * ln) . (upper_bound A)) - ((sec * ln) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) ) & Z c= dom (sec * ln) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((sec * ln) . (upper_bound A)) - ((sec * ln) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: sec * ln is_differentiable_on Z by A1, FDIFF_9:14; A4: for x being Real st x in dom ((sec * ln) `| Z) holds ((sec * ln) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((sec * ln) `| Z) implies ((sec * ln) `| Z) . x = f . x ) assume x in dom ((sec * ln) `| Z) ; ::_thesis: ((sec * ln) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((sec * ln) `| Z) . x = (sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) by A1, FDIFF_9:14 .= f . x by A1, A5 ; hence ((sec * ln) `| Z) . x = f . x ; ::_thesis: verum end; dom ((sec * ln) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (sec * ln) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((sec * ln) . (upper_bound A)) - ((sec * ln) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:20 for A being non empty closed_interval Subset of REAL for f 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 = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) & Z c= dom (cosec * ln) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * ln)) . (upper_bound A)) - ((- (cosec * ln)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) & Z c= dom (cosec * ln) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * ln)) . (upper_bound A)) - ((- (cosec * ln)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) & Z c= dom (cosec * ln) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * ln)) . (upper_bound A)) - ((- (cosec * ln)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) & Z c= dom (cosec * ln) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cosec * ln)) . (upper_bound A)) - ((- (cosec * ln)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) ) & Z c= dom (cosec * ln) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cosec * ln)) . (upper_bound A)) - ((- (cosec * ln)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (cosec * ln) is_differentiable_on Z by A1, Th3; A4: for x being Real st x in dom ((- (cosec * ln)) `| Z) holds ((- (cosec * ln)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (cosec * ln)) `| Z) implies ((- (cosec * ln)) `| Z) . x = f . x ) assume x in dom ((- (cosec * ln)) `| Z) ; ::_thesis: ((- (cosec * ln)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (cosec * ln)) `| Z) . x = (cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) by A1, Th3 .= f . x by A1, A5 ; hence ((- (cosec * ln)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (cosec * ln)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (cosec * ln)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (cosec * ln)) . (upper_bound A)) - ((- (cosec * ln)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:21 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (exp_R * sec) (#) (sin / (cos ^2)) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R * sec) . (upper_bound A)) - ((exp_R * sec) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (exp_R * sec) (#) (sin / (cos ^2)) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R * sec) . (upper_bound A)) - ((exp_R * sec) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = (exp_R * sec) (#) (sin / (cos ^2)) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R * sec) . (upper_bound A)) - ((exp_R * sec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = (exp_R * sec) (#) (sin / (cos ^2)) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R * sec) . (upper_bound A)) - ((exp_R * sec) . (lower_bound A)) ) assume A1: ( A c= Z & f = (exp_R * sec) (#) (sin / (cos ^2)) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R * sec) . (upper_bound A)) - ((exp_R * sec) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; Z = (dom (exp_R * sec)) /\ (dom (sin / (cos ^2))) by A1, VALUED_1:def_4; then A3: ( Z c= dom (exp_R * sec) & Z c= dom (sin / (cos ^2)) ) by XBOOLE_1:18; then A4: exp_R * sec is_differentiable_on Z by FDIFF_9:16; A5: for x being Real st x in Z holds f . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies f . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) assume A6: x in Z ; ::_thesis: f . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) ((exp_R * sec) (#) (sin / (cos ^2))) . x = ((exp_R * sec) . x) * ((sin / (cos ^2)) . x) by VALUED_1:5 .= (exp_R . (sec . x)) * ((sin / (cos ^2)) . x) by A6, A3, FUNCT_1:12 .= (exp_R . (sec . x)) * ((sin . x) / ((cos ^2) . x)) by A3, A6, RFUNCT_1:def_1 .= (exp_R . (sec . x)) * ((sin . x) / ((cos . x) ^2)) by VALUED_1:11 .= ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) ; hence f . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) by A1; ::_thesis: verum end; A7: for x being Real st x in dom ((exp_R * sec) `| Z) holds ((exp_R * sec) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((exp_R * sec) `| Z) implies ((exp_R * sec) `| Z) . x = f . x ) assume x in dom ((exp_R * sec) `| Z) ; ::_thesis: ((exp_R * sec) `| Z) . x = f . x then A8: x in Z by A4, FDIFF_1:def_7; then ((exp_R * sec) `| Z) . x = ((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) by A3, FDIFF_9:16 .= f . x by A5, A8 ; hence ((exp_R * sec) `| Z) . x = f . x ; ::_thesis: verum end; dom ((exp_R * sec) `| Z) = dom f by A1, A4, FDIFF_1:def_7; then (exp_R * sec) `| Z = f by A7, PARTFUN1:5; hence integral (f,A) = ((exp_R * sec) . (upper_bound A)) - ((exp_R * sec) . (lower_bound A)) by A1, A2, A4, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:22 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (exp_R * cosec) (#) (cos / (sin ^2)) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (exp_R * cosec)) . (upper_bound A)) - ((- (exp_R * cosec)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (exp_R * cosec) (#) (cos / (sin ^2)) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (exp_R * cosec)) . (upper_bound A)) - ((- (exp_R * cosec)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = (exp_R * cosec) (#) (cos / (sin ^2)) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (exp_R * cosec)) . (upper_bound A)) - ((- (exp_R * cosec)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = (exp_R * cosec) (#) (cos / (sin ^2)) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (exp_R * cosec)) . (upper_bound A)) - ((- (exp_R * cosec)) . (lower_bound A)) ) assume A1: ( A c= Z & f = (exp_R * cosec) (#) (cos / (sin ^2)) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (exp_R * cosec)) . (upper_bound A)) - ((- (exp_R * cosec)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; Z = (dom (exp_R * cosec)) /\ (dom (cos / (sin ^2))) by A1, VALUED_1:def_4; then A3: ( Z c= dom (exp_R * cosec) & Z c= dom (cos / (sin ^2)) ) by XBOOLE_1:18; then A4: - (exp_R * cosec) is_differentiable_on Z by Th4; A5: for x being Real st x in Z holds f . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies f . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ) assume A6: x in Z ; ::_thesis: f . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ((exp_R * cosec) (#) (cos / (sin ^2))) . x = ((exp_R * cosec) . x) * ((cos / (sin ^2)) . x) by VALUED_1:5 .= (exp_R . (cosec . x)) * ((cos / (sin ^2)) . x) by A6, A3, FUNCT_1:12 .= (exp_R . (cosec . x)) * ((cos . x) / ((sin ^2) . x)) by A3, A6, RFUNCT_1:def_1 .= (exp_R . (cosec . x)) * ((cos . x) / ((sin . x) ^2)) by VALUED_1:11 .= ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) ; hence f . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) by A1; ::_thesis: verum end; A7: for x being Real st x in dom ((- (exp_R * cosec)) `| Z) holds ((- (exp_R * cosec)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (exp_R * cosec)) `| Z) implies ((- (exp_R * cosec)) `| Z) . x = f . x ) assume x in dom ((- (exp_R * cosec)) `| Z) ; ::_thesis: ((- (exp_R * cosec)) `| Z) . x = f . x then A8: x in Z by A4, FDIFF_1:def_7; then ((- (exp_R * cosec)) `| Z) . x = ((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) by A3, Th4 .= f . x by A5, A8 ; hence ((- (exp_R * cosec)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (exp_R * cosec)) `| Z) = dom f by A1, A4, FDIFF_1:def_7; then (- (exp_R * cosec)) `| Z = f by A7, PARTFUN1:5; hence integral (f,A) = ((- (exp_R * cosec)) . (upper_bound A)) - ((- (exp_R * cosec)) . (lower_bound A)) by A1, A2, A4, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:23 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & Z c= dom (ln * sec) & Z = dom tan & tan | A is continuous holds integral (tan,A) = ((ln * sec) . (upper_bound A)) - ((ln * sec) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & Z c= dom (ln * sec) & Z = dom tan & tan | A is continuous holds integral (tan,A) = ((ln * sec) . (upper_bound A)) - ((ln * sec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & Z c= dom (ln * sec) & Z = dom tan & tan | A is continuous implies integral (tan,A) = ((ln * sec) . (upper_bound A)) - ((ln * sec) . (lower_bound A)) ) assume A1: ( A c= Z & Z c= dom (ln * sec) & Z = dom tan & tan | A is continuous ) ; ::_thesis: integral (tan,A) = ((ln * sec) . (upper_bound A)) - ((ln * sec) . (lower_bound A)) then A2: ( tan is_integrable_on A & tan | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: ln * sec is_differentiable_on Z by A1, FDIFF_9:18; A4: for x being Real st x in Z holds cos . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies cos . x <> 0 ) assume x in Z ; ::_thesis: cos . x <> 0 then x in dom sec by A1, FUNCT_1:11; hence cos . x <> 0 by RFUNCT_1:3; ::_thesis: verum end; A5: for x being Real st x in dom ((ln * sec) `| Z) holds ((ln * sec) `| Z) . x = tan . x proof let x be Real; ::_thesis: ( x in dom ((ln * sec) `| Z) implies ((ln * sec) `| Z) . x = tan . x ) assume x in dom ((ln * sec) `| Z) ; ::_thesis: ((ln * sec) `| Z) . x = tan . x then A6: x in Z by A3, FDIFF_1:def_7; then A7: cos . x <> 0 by A4; ((ln * sec) `| Z) . x = tan x by A1, A6, FDIFF_9:18 .= tan . x by A7, SIN_COS9:15 ; hence ((ln * sec) `| Z) . x = tan . x ; ::_thesis: verum end; dom ((ln * sec) `| Z) = dom tan by A1, A3, FDIFF_1:def_7; then (ln * sec) `| Z = tan by A5, PARTFUN1:5; hence integral (tan,A) = ((ln * sec) . (upper_bound A)) - ((ln * sec) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:24 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & Z c= dom (ln * cosec) & Z = dom cot & (- cot) | A is continuous holds integral ((- cot),A) = ((ln * cosec) . (upper_bound A)) - ((ln * cosec) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & Z c= dom (ln * cosec) & Z = dom cot & (- cot) | A is continuous holds integral ((- cot),A) = ((ln * cosec) . (upper_bound A)) - ((ln * cosec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & Z c= dom (ln * cosec) & Z = dom cot & (- cot) | A is continuous implies integral ((- cot),A) = ((ln * cosec) . (upper_bound A)) - ((ln * cosec) . (lower_bound A)) ) assume A1: ( A c= Z & Z c= dom (ln * cosec) & Z = dom cot & (- cot) | A is continuous ) ; ::_thesis: integral ((- cot),A) = ((ln * cosec) . (upper_bound A)) - ((ln * cosec) . (lower_bound A)) then A2: Z = dom (- cot) by VALUED_1:8; then A3: ( - cot is_integrable_on A & (- cot) | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11; A4: ln * cosec is_differentiable_on Z by A1, FDIFF_9:19; A5: for x being Real st x in Z holds sin . x <> 0 proof let x be Real; ::_thesis: ( x in Z implies sin . x <> 0 ) assume x in Z ; ::_thesis: sin . x <> 0 then x in dom cosec by A1, FUNCT_1:11; hence sin . x <> 0 by RFUNCT_1:3; ::_thesis: verum end; A6: for x being Real st x in dom ((ln * cosec) `| Z) holds ((ln * cosec) `| Z) . x = (- cot) . x proof let x be Real; ::_thesis: ( x in dom ((ln * cosec) `| Z) implies ((ln * cosec) `| Z) . x = (- cot) . x ) assume x in dom ((ln * cosec) `| Z) ; ::_thesis: ((ln * cosec) `| Z) . x = (- cot) . x then A7: x in Z by A4, FDIFF_1:def_7; then A8: sin . x <> 0 by A5; ((ln * cosec) `| Z) . x = - (cot x) by A1, A7, FDIFF_9:19 .= - (cot . x) by A8, SIN_COS9:16 .= (- cot) . x by VALUED_1:8 ; hence ((ln * cosec) `| Z) . x = (- cot) . x ; ::_thesis: verum end; dom ((ln * cosec) `| Z) = dom (- cot) by A2, A4, FDIFF_1:def_7; then (ln * cosec) `| Z = - cot by A6, PARTFUN1:5; hence integral ((- cot),A) = ((ln * cosec) . (upper_bound A)) - ((ln * cosec) . (lower_bound A)) by A1, A3, A4, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:25 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & Z c= dom (ln * cosec) & Z = dom cot & cot | A is continuous holds integral (cot,A) = ((- (ln * cosec)) . (upper_bound A)) - ((- (ln * cosec)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & Z c= dom (ln * cosec) & Z = dom cot & cot | A is continuous holds integral (cot,A) = ((- (ln * cosec)) . (upper_bound A)) - ((- (ln * cosec)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & Z c= dom (ln * cosec) & Z = dom cot & cot | A is continuous implies integral (cot,A) = ((- (ln * cosec)) . (upper_bound A)) - ((- (ln * cosec)) . (lower_bound A)) ) assume A1: ( A c= Z & Z c= dom (ln * cosec) & Z = dom cot & cot | A is continuous ) ; ::_thesis: integral (cot,A) = ((- (ln * cosec)) . (upper_bound A)) - ((- (ln * cosec)) . (lower_bound A)) then A2: ( cot is_integrable_on A & cot | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (ln * cosec) is_differentiable_on Z by A1, Th5; A4: for x being Real st x in dom ((- (ln * cosec)) `| Z) holds ((- (ln * cosec)) `| Z) . x = cot . x proof let x be Real; ::_thesis: ( x in dom ((- (ln * cosec)) `| Z) implies ((- (ln * cosec)) `| Z) . x = cot . x ) assume x in dom ((- (ln * cosec)) `| Z) ; ::_thesis: ((- (ln * cosec)) `| Z) . x = cot . x then x in Z by A3, FDIFF_1:def_7; then ((- (ln * cosec)) `| Z) . x = cot . x by A1, Th5; hence ((- (ln * cosec)) `| Z) . x = cot . x ; ::_thesis: verum end; dom ((- (ln * cosec)) `| Z) = dom cot by A1, A3, FDIFF_1:def_7; then (- (ln * cosec)) `| Z = cot by A4, PARTFUN1:5; hence integral (cot,A) = ((- (ln * cosec)) . (upper_bound A)) - ((- (ln * cosec)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:26 for n being Nat for A being non empty closed_interval Subset of REAL for f 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 = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * sec) & 1 <= n & Z = dom f & f | A is continuous holds integral (f,A) = (((#Z n) * sec) . (upper_bound A)) - (((#Z n) * sec) . (lower_bound A)) proof let n be Nat; ::_thesis: for A being non empty closed_interval Subset of REAL for f 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 = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * sec) & 1 <= n & Z = dom f & f | A is continuous holds integral (f,A) = (((#Z n) * sec) . (upper_bound A)) - (((#Z n) * sec) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * sec) & 1 <= n & Z = dom f & f | A is continuous holds integral (f,A) = (((#Z n) * sec) . (upper_bound A)) - (((#Z n) * sec) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * sec) & 1 <= n & Z = dom f & f | A is continuous holds integral (f,A) = (((#Z n) * sec) . (upper_bound A)) - (((#Z n) * sec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * sec) & 1 <= n & Z = dom f & f | A is continuous implies integral (f,A) = (((#Z n) * sec) . (upper_bound A)) - (((#Z n) * sec) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * sec) & 1 <= n & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = (((#Z n) * sec) . (upper_bound A)) - (((#Z n) * sec) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: (#Z n) * sec is_differentiable_on Z by A1, FDIFF_9:20; A4: for x being Real st x in dom (((#Z n) * sec) `| Z) holds (((#Z n) * sec) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom (((#Z n) * sec) `| Z) implies (((#Z n) * sec) `| Z) . x = f . x ) assume x in dom (((#Z n) * sec) `| Z) ; ::_thesis: (((#Z n) * sec) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then (((#Z n) * sec) `| Z) . x = (n * (sin . x)) / ((cos . x) #Z (n + 1)) by A1, FDIFF_9:20 .= f . x by A1, A5 ; hence (((#Z n) * sec) `| Z) . x = f . x ; ::_thesis: verum end; dom (((#Z n) * sec) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then ((#Z n) * sec) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = (((#Z n) * sec) . (upper_bound A)) - (((#Z n) * sec) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:27 for n being Nat for A being non empty closed_interval Subset of REAL for f 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 = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * cosec) & 1 <= n & Z = dom f & f | A is continuous holds integral (f,A) = ((- ((#Z n) * cosec)) . (upper_bound A)) - ((- ((#Z n) * cosec)) . (lower_bound A)) proof let n be Nat; ::_thesis: for A being non empty closed_interval Subset of REAL for f 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 = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * cosec) & 1 <= n & Z = dom f & f | A is continuous holds integral (f,A) = ((- ((#Z n) * cosec)) . (upper_bound A)) - ((- ((#Z n) * cosec)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * cosec) & 1 <= n & Z = dom f & f | A is continuous holds integral (f,A) = ((- ((#Z n) * cosec)) . (upper_bound A)) - ((- ((#Z n) * cosec)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * cosec) & 1 <= n & Z = dom f & f | A is continuous holds integral (f,A) = ((- ((#Z n) * cosec)) . (upper_bound A)) - ((- ((#Z n) * cosec)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * cosec) & 1 <= n & Z = dom f & f | A is continuous implies integral (f,A) = ((- ((#Z n) * cosec)) . (upper_bound A)) - ((- ((#Z n) * cosec)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) & Z c= dom ((#Z n) * cosec) & 1 <= n & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- ((#Z n) * cosec)) . (upper_bound A)) - ((- ((#Z n) * cosec)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - ((#Z n) * cosec) is_differentiable_on Z by A1, Th6; A4: for x being Real st x in dom ((- ((#Z n) * cosec)) `| Z) holds ((- ((#Z n) * cosec)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- ((#Z n) * cosec)) `| Z) implies ((- ((#Z n) * cosec)) `| Z) . x = f . x ) assume x in dom ((- ((#Z n) * cosec)) `| Z) ; ::_thesis: ((- ((#Z n) * cosec)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) by A1, Th6 .= f . x by A1, A5 ; hence ((- ((#Z n) * cosec)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- ((#Z n) * cosec)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- ((#Z n) * cosec)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- ((#Z n) * cosec)) . (upper_bound A)) - ((- ((#Z n) * cosec)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:28 for A being non empty closed_interval Subset of REAL for f 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 = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (exp_R (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) sec) . (upper_bound A)) - ((exp_R (#) sec) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (exp_R (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) sec) . (upper_bound A)) - ((exp_R (#) sec) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (exp_R (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) sec) . (upper_bound A)) - ((exp_R (#) sec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (exp_R (#) sec) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R (#) sec) . (upper_bound A)) - ((exp_R (#) sec) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (exp_R (#) sec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R (#) sec) . (upper_bound A)) - ((exp_R (#) sec) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: exp_R (#) sec is_differentiable_on Z by A1, FDIFF_9:24; A4: for x being Real st x in dom ((exp_R (#) sec) `| Z) holds ((exp_R (#) sec) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((exp_R (#) sec) `| Z) implies ((exp_R (#) sec) `| Z) . x = f . x ) assume x in dom ((exp_R (#) sec) `| Z) ; ::_thesis: ((exp_R (#) sec) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((exp_R (#) sec) `| Z) . x = ((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) by A1, FDIFF_9:24 .= f . x by A1, A5 ; hence ((exp_R (#) sec) `| Z) . x = f . x ; ::_thesis: verum end; dom ((exp_R (#) sec) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (exp_R (#) sec) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((exp_R (#) sec) . (upper_bound A)) - ((exp_R (#) sec) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:29 for A being non empty closed_interval Subset of REAL for f 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 = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (exp_R (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) cosec) . (upper_bound A)) - ((exp_R (#) cosec) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (exp_R (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) cosec) . (upper_bound A)) - ((exp_R (#) cosec) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (exp_R (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) cosec) . (upper_bound A)) - ((exp_R (#) cosec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (exp_R (#) cosec) & Z = dom f & f | A is continuous implies integral (f,A) = ((exp_R (#) cosec) . (upper_bound A)) - ((exp_R (#) cosec) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (exp_R (#) cosec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((exp_R (#) cosec) . (upper_bound A)) - ((exp_R (#) cosec) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: exp_R (#) cosec is_differentiable_on Z by A1, FDIFF_9:25; A4: for x being Real st x in dom ((exp_R (#) cosec) `| Z) holds ((exp_R (#) cosec) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((exp_R (#) cosec) `| Z) implies ((exp_R (#) cosec) `| Z) . x = f . x ) assume x in dom ((exp_R (#) cosec) `| Z) ; ::_thesis: ((exp_R (#) cosec) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((exp_R (#) cosec) `| Z) . x = ((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) by A1, FDIFF_9:25 .= f . x by A1, A5 ; hence ((exp_R (#) cosec) `| Z) . x = f . x ; ::_thesis: verum end; dom ((exp_R (#) cosec) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (exp_R (#) cosec) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((exp_R (#) cosec) . (upper_bound A)) - ((exp_R (#) cosec) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:30 for a being 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 = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) & Z c= dom (((1 / a) (#) (sec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((1 / a) (#) (sec * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (sec * f1)) - (id Z)) . (lower_bound A)) proof let a be Real; ::_thesis: 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 = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) & Z c= dom (((1 / a) (#) (sec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((1 / a) (#) (sec * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (sec * f1)) - (id Z)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: 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 = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) & Z c= dom (((1 / a) (#) (sec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((1 / a) (#) (sec * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (sec * f1)) - (id Z)) . (lower_bound A)) let f, f1 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) & Z c= dom (((1 / a) (#) (sec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((1 / a) (#) (sec * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (sec * f1)) - (id Z)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) & Z c= dom (((1 / a) (#) (sec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous implies integral (f,A) = ((((1 / a) (#) (sec * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (sec * f1)) - (id Z)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) ) & Z c= dom (((1 / a) (#) (sec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((((1 / a) (#) (sec * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (sec * f1)) - (id Z)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: ((1 / a) (#) (sec * f1)) - (id Z) is_differentiable_on Z by A1, FDIFF_9:26; A4: for x being Real st x in dom ((((1 / a) (#) (sec * f1)) - (id Z)) `| Z) holds ((((1 / a) (#) (sec * f1)) - (id Z)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((((1 / a) (#) (sec * f1)) - (id Z)) `| Z) implies ((((1 / a) (#) (sec * f1)) - (id Z)) `| Z) . x = f . x ) assume x in dom ((((1 / a) (#) (sec * f1)) - (id Z)) `| Z) ; ::_thesis: ((((1 / a) (#) (sec * f1)) - (id Z)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((((1 / a) (#) (sec * f1)) - (id Z)) `| Z) . x = ((sin . (a * x)) - ((cos . (a * x)) ^2)) / ((cos . (a * x)) ^2) by A1, FDIFF_9:26 .= f . x by A1, A5 ; hence ((((1 / a) (#) (sec * f1)) - (id Z)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((((1 / a) (#) (sec * f1)) - (id Z)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (((1 / a) (#) (sec * f1)) - (id Z)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((((1 / a) (#) (sec * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (sec * f1)) - (id Z)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:31 for a being 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 = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) & Z c= dom (((- (1 / a)) (#) (cosec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (lower_bound A)) proof let a be Real; ::_thesis: 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 = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) & Z c= dom (((- (1 / a)) (#) (cosec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: 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 = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) & Z c= dom (((- (1 / a)) (#) (cosec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (lower_bound A)) let f, f1 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) & Z c= dom (((- (1 / a)) (#) (cosec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) & Z c= dom (((- (1 / a)) (#) (cosec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous implies integral (f,A) = ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) ) & Z c= dom (((- (1 / a)) (#) (cosec * f1)) - (id Z)) & ( for x being Real st x in Z holds ( f1 . x = a * x & a <> 0 ) ) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: ((- (1 / a)) (#) (cosec * f1)) - (id Z) is_differentiable_on Z by A1, FDIFF_9:27; A4: for x being Real st x in dom ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z) holds ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z) implies ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z) . x = f . x ) assume x in dom ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z) ; ::_thesis: ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z) . x = ((cos . (a * x)) - ((sin . (a * x)) ^2)) / ((sin . (a * x)) ^2) by A1, FDIFF_9:27 .= f . x by A1, A5 ; hence ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (((- (1 / a)) (#) (cosec * f1)) - (id Z)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (upper_bound A)) - ((((- (1 / a)) (#) (cosec * f1)) - (id Z)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:32 for A being non empty closed_interval Subset of REAL for f 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 = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (ln (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) sec) . (upper_bound A)) - ((ln (#) sec) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (ln (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) sec) . (upper_bound A)) - ((ln (#) sec) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (ln (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) sec) . (upper_bound A)) - ((ln (#) sec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (ln (#) sec) & Z = dom f & f | A is continuous implies integral (f,A) = ((ln (#) sec) . (upper_bound A)) - ((ln (#) sec) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (ln (#) sec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((ln (#) sec) . (upper_bound A)) - ((ln (#) sec) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: ln (#) sec is_differentiable_on Z by A1, FDIFF_9:30; A4: for x being Real st x in dom ((ln (#) sec) `| Z) holds ((ln (#) sec) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((ln (#) sec) `| Z) implies ((ln (#) sec) `| Z) . x = f . x ) assume x in dom ((ln (#) sec) `| Z) ; ::_thesis: ((ln (#) sec) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((ln (#) sec) `| Z) . x = ((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) by A1, FDIFF_9:30 .= f . x by A1, A5 ; hence ((ln (#) sec) `| Z) . x = f . x ; ::_thesis: verum end; dom ((ln (#) sec) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (ln (#) sec) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((ln (#) sec) . (upper_bound A)) - ((ln (#) sec) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:33 for A being non empty closed_interval Subset of REAL for f 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 = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (ln (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) cosec) . (upper_bound A)) - ((ln (#) cosec) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (ln (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) cosec) . (upper_bound A)) - ((ln (#) cosec) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (ln (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) cosec) . (upper_bound A)) - ((ln (#) cosec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (ln (#) cosec) & Z = dom f & f | A is continuous implies integral (f,A) = ((ln (#) cosec) . (upper_bound A)) - ((ln (#) cosec) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (ln (#) cosec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((ln (#) cosec) . (upper_bound A)) - ((ln (#) cosec) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: ln (#) cosec is_differentiable_on Z by A1, FDIFF_9:31; A4: for x being Real st x in dom ((ln (#) cosec) `| Z) holds ((ln (#) cosec) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((ln (#) cosec) `| Z) implies ((ln (#) cosec) `| Z) . x = f . x ) assume x in dom ((ln (#) cosec) `| Z) ; ::_thesis: ((ln (#) cosec) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((ln (#) cosec) `| Z) . x = ((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) by A1, FDIFF_9:31 .= f . x by A1, A5 ; hence ((ln (#) cosec) `| Z) . x = f . x ; ::_thesis: verum end; dom ((ln (#) cosec) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (ln (#) cosec) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((ln (#) cosec) . (upper_bound A)) - ((ln (#) cosec) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:34 for A being non empty closed_interval Subset of REAL for f 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 = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) & Z c= dom (((id Z) ^) (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (((id Z) ^) (#) sec)) . (upper_bound A)) - ((- (((id Z) ^) (#) sec)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) & Z c= dom (((id Z) ^) (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (((id Z) ^) (#) sec)) . (upper_bound A)) - ((- (((id Z) ^) (#) sec)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) & Z c= dom (((id Z) ^) (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (((id Z) ^) (#) sec)) . (upper_bound A)) - ((- (((id Z) ^) (#) sec)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) & Z c= dom (((id Z) ^) (#) sec) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (((id Z) ^) (#) sec)) . (upper_bound A)) - ((- (((id Z) ^) (#) sec)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) ) & Z c= dom (((id Z) ^) (#) sec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (((id Z) ^) (#) sec)) . (upper_bound A)) - ((- (((id Z) ^) (#) sec)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (((id Z) ^) (#) sec) is_differentiable_on Z by A1, Th7; A4: for x being Real st x in dom ((- (((id Z) ^) (#) sec)) `| Z) holds ((- (((id Z) ^) (#) sec)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (((id Z) ^) (#) sec)) `| Z) implies ((- (((id Z) ^) (#) sec)) `| Z) . x = f . x ) assume x in dom ((- (((id Z) ^) (#) sec)) `| Z) ; ::_thesis: ((- (((id Z) ^) (#) sec)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (((id Z) ^) (#) sec)) `| Z) . x = ((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) by A1, Th7 .= f . x by A1, A5 ; hence ((- (((id Z) ^) (#) sec)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (((id Z) ^) (#) sec)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (((id Z) ^) (#) sec)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (((id Z) ^) (#) sec)) . (upper_bound A)) - ((- (((id Z) ^) (#) sec)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:35 for A being non empty closed_interval Subset of REAL for f 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 = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) & Z c= dom (((id Z) ^) (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (((id Z) ^) (#) cosec)) . (upper_bound A)) - ((- (((id Z) ^) (#) cosec)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) & Z c= dom (((id Z) ^) (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (((id Z) ^) (#) cosec)) . (upper_bound A)) - ((- (((id Z) ^) (#) cosec)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) & Z c= dom (((id Z) ^) (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (((id Z) ^) (#) cosec)) . (upper_bound A)) - ((- (((id Z) ^) (#) cosec)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) & Z c= dom (((id Z) ^) (#) cosec) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (((id Z) ^) (#) cosec)) . (upper_bound A)) - ((- (((id Z) ^) (#) cosec)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) ) & Z c= dom (((id Z) ^) (#) cosec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (((id Z) ^) (#) cosec)) . (upper_bound A)) - ((- (((id Z) ^) (#) cosec)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (((id Z) ^) (#) cosec) is_differentiable_on Z by A1, Th8; A4: for x being Real st x in dom ((- (((id Z) ^) (#) cosec)) `| Z) holds ((- (((id Z) ^) (#) cosec)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (((id Z) ^) (#) cosec)) `| Z) implies ((- (((id Z) ^) (#) cosec)) `| Z) . x = f . x ) assume x in dom ((- (((id Z) ^) (#) cosec)) `| Z) ; ::_thesis: ((- (((id Z) ^) (#) cosec)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (((id Z) ^) (#) cosec)) `| Z) . x = ((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) by A1, Th8 .= f . x by A1, A5 ; hence ((- (((id Z) ^) (#) cosec)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (((id Z) ^) (#) cosec)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (((id Z) ^) (#) cosec)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (((id Z) ^) (#) cosec)) . (upper_bound A)) - ((- (((id Z) ^) (#) cosec)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:36 for A being non empty closed_interval Subset of REAL for f 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 = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) & Z c= dom (sec * sin) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * sin) . (upper_bound A)) - ((sec * sin) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) & Z c= dom (sec * sin) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * sin) . (upper_bound A)) - ((sec * sin) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) & Z c= dom (sec * sin) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * sin) . (upper_bound A)) - ((sec * sin) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) & Z c= dom (sec * sin) & Z = dom f & f | A is continuous implies integral (f,A) = ((sec * sin) . (upper_bound A)) - ((sec * sin) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) ) & Z c= dom (sec * sin) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((sec * sin) . (upper_bound A)) - ((sec * sin) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: sec * sin is_differentiable_on Z by A1, FDIFF_9:34; A4: for x being Real st x in dom ((sec * sin) `| Z) holds ((sec * sin) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((sec * sin) `| Z) implies ((sec * sin) `| Z) . x = f . x ) assume x in dom ((sec * sin) `| Z) ; ::_thesis: ((sec * sin) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((sec * sin) `| Z) . x = ((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) by A1, FDIFF_9:34 .= f . x by A1, A5 ; hence ((sec * sin) `| Z) . x = f . x ; ::_thesis: verum end; dom ((sec * sin) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (sec * sin) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((sec * sin) . (upper_bound A)) - ((sec * sin) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:37 for A being non empty closed_interval Subset of REAL for f 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 = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ) & Z c= dom (sec * cos) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sec * cos)) . (upper_bound A)) - ((- (sec * cos)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ) & Z c= dom (sec * cos) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sec * cos)) . (upper_bound A)) - ((- (sec * cos)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ) & Z c= dom (sec * cos) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sec * cos)) . (upper_bound A)) - ((- (sec * cos)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ) & Z c= dom (sec * cos) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (sec * cos)) . (upper_bound A)) - ((- (sec * cos)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ) & Z c= dom (sec * cos) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (sec * cos)) . (upper_bound A)) - ((- (sec * cos)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: Z c= dom (- (sec * cos)) by A1, VALUED_1:8; A4: sec * cos is_differentiable_on Z by A1, FDIFF_9:35; then A5: (- 1) (#) (sec * cos) is_differentiable_on Z by A3, FDIFF_1:20; A6: for x being Real st x in Z holds ((- (sec * cos)) `| Z) . x = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((- (sec * cos)) `| Z) . x = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ) assume A7: x in Z ; ::_thesis: ((- (sec * cos)) `| Z) . x = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ((- (sec * cos)) `| Z) . x = ((- 1) (#) ((sec * cos) `| Z)) . x by A4, FDIFF_2:19 .= (- 1) * (((sec * cos) `| Z) . x) by VALUED_1:6 .= (- 1) * (- (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2))) by A1, A7, FDIFF_9:35 .= ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ; hence ((- (sec * cos)) `| Z) . x = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) ; ::_thesis: verum end; A8: for x being Real st x in dom ((- (sec * cos)) `| Z) holds ((- (sec * cos)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (sec * cos)) `| Z) implies ((- (sec * cos)) `| Z) . x = f . x ) assume x in dom ((- (sec * cos)) `| Z) ; ::_thesis: ((- (sec * cos)) `| Z) . x = f . x then A9: x in Z by A5, FDIFF_1:def_7; then ((- (sec * cos)) `| Z) . x = ((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) by A6 .= f . x by A1, A9 ; hence ((- (sec * cos)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (sec * cos)) `| Z) = dom f by A1, A5, FDIFF_1:def_7; then (- (sec * cos)) `| Z = f by A8, PARTFUN1:5; hence integral (f,A) = ((- (sec * cos)) . (upper_bound A)) - ((- (sec * cos)) . (lower_bound A)) by A1, A2, A5, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:38 for A being non empty closed_interval Subset of REAL for f 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 = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) & Z c= dom (cosec * sin) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * sin)) . (upper_bound A)) - ((- (cosec * sin)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) & Z c= dom (cosec * sin) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * sin)) . (upper_bound A)) - ((- (cosec * sin)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) & Z c= dom (cosec * sin) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * sin)) . (upper_bound A)) - ((- (cosec * sin)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) & Z c= dom (cosec * sin) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cosec * sin)) . (upper_bound A)) - ((- (cosec * sin)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) ) & Z c= dom (cosec * sin) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cosec * sin)) . (upper_bound A)) - ((- (cosec * sin)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (cosec * sin) is_differentiable_on Z by A1, Th9; A4: for x being Real st x in dom ((- (cosec * sin)) `| Z) holds ((- (cosec * sin)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (cosec * sin)) `| Z) implies ((- (cosec * sin)) `| Z) . x = f . x ) assume x in dom ((- (cosec * sin)) `| Z) ; ::_thesis: ((- (cosec * sin)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (cosec * sin)) `| Z) . x = ((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) by A1, Th9 .= f . x by A1, A5 ; hence ((- (cosec * sin)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (cosec * sin)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (cosec * sin)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (cosec * sin)) . (upper_bound A)) - ((- (cosec * sin)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:39 for A being non empty closed_interval Subset of REAL for f 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 = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) & Z c= dom (cosec * cos) & Z = dom f & f | A is continuous holds integral (f,A) = ((cosec * cos) . (upper_bound A)) - ((cosec * cos) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) & Z c= dom (cosec * cos) & Z = dom f & f | A is continuous holds integral (f,A) = ((cosec * cos) . (upper_bound A)) - ((cosec * cos) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) & Z c= dom (cosec * cos) & Z = dom f & f | A is continuous holds integral (f,A) = ((cosec * cos) . (upper_bound A)) - ((cosec * cos) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) & Z c= dom (cosec * cos) & Z = dom f & f | A is continuous implies integral (f,A) = ((cosec * cos) . (upper_bound A)) - ((cosec * cos) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) ) & Z c= dom (cosec * cos) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((cosec * cos) . (upper_bound A)) - ((cosec * cos) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: cosec * cos is_differentiable_on Z by A1, FDIFF_9:37; A4: for x being Real st x in dom ((cosec * cos) `| Z) holds ((cosec * cos) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((cosec * cos) `| Z) implies ((cosec * cos) `| Z) . x = f . x ) assume x in dom ((cosec * cos) `| Z) ; ::_thesis: ((cosec * cos) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((cosec * cos) `| Z) . x = ((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) by A1, FDIFF_9:37 .= f . x by A1, A5 ; hence ((cosec * cos) `| Z) . x = f . x ; ::_thesis: verum end; dom ((cosec * cos) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (cosec * cos) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((cosec * cos) . (upper_bound A)) - ((cosec * cos) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:40 for A being non empty closed_interval Subset of REAL for f 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 = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) & Z c= dom (sec * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * tan) . (upper_bound A)) - ((sec * tan) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) & Z c= dom (sec * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * tan) . (upper_bound A)) - ((sec * tan) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) & Z c= dom (sec * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((sec * tan) . (upper_bound A)) - ((sec * tan) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) & Z c= dom (sec * tan) & Z = dom f & f | A is continuous implies integral (f,A) = ((sec * tan) . (upper_bound A)) - ((sec * tan) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) ) & Z c= dom (sec * tan) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((sec * tan) . (upper_bound A)) - ((sec * tan) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: sec * tan is_differentiable_on Z by A1, FDIFF_9:38; A4: for x being Real st x in dom ((sec * tan) `| Z) holds ((sec * tan) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((sec * tan) `| Z) implies ((sec * tan) `| Z) . x = f . x ) assume x in dom ((sec * tan) `| Z) ; ::_thesis: ((sec * tan) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((sec * tan) `| Z) . x = ((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) by A1, FDIFF_9:38 .= f . x by A1, A5 ; hence ((sec * tan) `| Z) . x = f . x ; ::_thesis: verum end; dom ((sec * tan) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (sec * tan) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((sec * tan) . (upper_bound A)) - ((sec * tan) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:41 for A being non empty closed_interval Subset of REAL for f 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 = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) & Z c= dom (sec * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sec * cot)) . (upper_bound A)) - ((- (sec * cot)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) & Z c= dom (sec * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sec * cot)) . (upper_bound A)) - ((- (sec * cot)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) & Z c= dom (sec * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sec * cot)) . (upper_bound A)) - ((- (sec * cot)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) & Z c= dom (sec * cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (sec * cot)) . (upper_bound A)) - ((- (sec * cot)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) ) & Z c= dom (sec * cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (sec * cot)) . (upper_bound A)) - ((- (sec * cot)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (sec * cot) is_differentiable_on Z by A1, Th10; A4: for x being Real st x in dom ((- (sec * cot)) `| Z) holds ((- (sec * cot)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (sec * cot)) `| Z) implies ((- (sec * cot)) `| Z) . x = f . x ) assume x in dom ((- (sec * cot)) `| Z) ; ::_thesis: ((- (sec * cot)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (sec * cot)) `| Z) . x = ((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) by A1, Th10 .= f . x by A1, A5 ; hence ((- (sec * cot)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (sec * cot)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (sec * cot)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (sec * cot)) . (upper_bound A)) - ((- (sec * cot)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:42 for A being non empty closed_interval Subset of REAL for f 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 = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) & Z c= dom (cosec * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * tan)) . (upper_bound A)) - ((- (cosec * tan)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) & Z c= dom (cosec * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * tan)) . (upper_bound A)) - ((- (cosec * tan)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) & Z c= dom (cosec * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cosec * tan)) . (upper_bound A)) - ((- (cosec * tan)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) & Z c= dom (cosec * tan) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cosec * tan)) . (upper_bound A)) - ((- (cosec * tan)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) ) & Z c= dom (cosec * tan) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cosec * tan)) . (upper_bound A)) - ((- (cosec * tan)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (cosec * tan) is_differentiable_on Z by A1, Th11; A4: for x being Real st x in dom ((- (cosec * tan)) `| Z) holds ((- (cosec * tan)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (cosec * tan)) `| Z) implies ((- (cosec * tan)) `| Z) . x = f . x ) assume x in dom ((- (cosec * tan)) `| Z) ; ::_thesis: ((- (cosec * tan)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (cosec * tan)) `| Z) . x = ((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) by A1, Th11 .= f . x by A1, A5 ; hence ((- (cosec * tan)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (cosec * tan)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (cosec * tan)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (cosec * tan)) . (upper_bound A)) - ((- (cosec * tan)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:43 for A being non empty closed_interval Subset of REAL for f 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 = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) & Z c= dom (cosec * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((cosec * cot) . (upper_bound A)) - ((cosec * cot) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) & Z c= dom (cosec * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((cosec * cot) . (upper_bound A)) - ((cosec * cot) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) & Z c= dom (cosec * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((cosec * cot) . (upper_bound A)) - ((cosec * cot) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) & Z c= dom (cosec * cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((cosec * cot) . (upper_bound A)) - ((cosec * cot) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) ) & Z c= dom (cosec * cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((cosec * cot) . (upper_bound A)) - ((cosec * cot) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: cosec * cot is_differentiable_on Z by A1, FDIFF_9:41; A4: for x being Real st x in dom ((cosec * cot) `| Z) holds ((cosec * cot) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((cosec * cot) `| Z) implies ((cosec * cot) `| Z) . x = f . x ) assume x in dom ((cosec * cot) `| Z) ; ::_thesis: ((cosec * cot) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((cosec * cot) `| Z) . x = ((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) by A1, FDIFF_9:41 .= f . x by A1, A5 ; hence ((cosec * cot) `| Z) . x = f . x ; ::_thesis: verum end; dom ((cosec * cot) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (cosec * cot) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((cosec * cot) . (upper_bound A)) - ((cosec * cot) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:44 for A being non empty closed_interval Subset of REAL for f 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 = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (tan (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan (#) sec) . (upper_bound A)) - ((tan (#) sec) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (tan (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan (#) sec) . (upper_bound A)) - ((tan (#) sec) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (tan (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan (#) sec) . (upper_bound A)) - ((tan (#) sec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (tan (#) sec) & Z = dom f & f | A is continuous implies integral (f,A) = ((tan (#) sec) . (upper_bound A)) - ((tan (#) sec) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (tan (#) sec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((tan (#) sec) . (upper_bound A)) - ((tan (#) sec) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: tan (#) sec is_differentiable_on Z by A1, FDIFF_9:42; A4: for x being Real st x in dom ((tan (#) sec) `| Z) holds ((tan (#) sec) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((tan (#) sec) `| Z) implies ((tan (#) sec) `| Z) . x = f . x ) assume x in dom ((tan (#) sec) `| Z) ; ::_thesis: ((tan (#) sec) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((tan (#) sec) `| Z) . x = ((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) by A1, FDIFF_9:42 .= f . x by A1, A5 ; hence ((tan (#) sec) `| Z) . x = f . x ; ::_thesis: verum end; dom ((tan (#) sec) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (tan (#) sec) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((tan (#) sec) . (upper_bound A)) - ((tan (#) sec) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:45 for A being non empty closed_interval Subset of REAL for f 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 = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (cot (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot (#) sec)) . (upper_bound A)) - ((- (cot (#) sec)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (cot (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot (#) sec)) . (upper_bound A)) - ((- (cot (#) sec)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (cot (#) sec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot (#) sec)) . (upper_bound A)) - ((- (cot (#) sec)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (cot (#) sec) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cot (#) sec)) . (upper_bound A)) - ((- (cot (#) sec)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) ) & Z c= dom (cot (#) sec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cot (#) sec)) . (upper_bound A)) - ((- (cot (#) sec)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (cot (#) sec) is_differentiable_on Z by A1, Th12; A4: for x being Real st x in dom ((- (cot (#) sec)) `| Z) holds ((- (cot (#) sec)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (cot (#) sec)) `| Z) implies ((- (cot (#) sec)) `| Z) . x = f . x ) assume x in dom ((- (cot (#) sec)) `| Z) ; ::_thesis: ((- (cot (#) sec)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (cot (#) sec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) by A1, Th12 .= f . x by A1, A5 ; hence ((- (cot (#) sec)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (cot (#) sec)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (cot (#) sec)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (cot (#) sec)) . (upper_bound A)) - ((- (cot (#) sec)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:46 for A being non empty closed_interval Subset of REAL for f 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 = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (tan (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan (#) cosec) . (upper_bound A)) - ((tan (#) cosec) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (tan (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan (#) cosec) . (upper_bound A)) - ((tan (#) cosec) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (tan (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan (#) cosec) . (upper_bound A)) - ((tan (#) cosec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (tan (#) cosec) & Z = dom f & f | A is continuous implies integral (f,A) = ((tan (#) cosec) . (upper_bound A)) - ((tan (#) cosec) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (tan (#) cosec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((tan (#) cosec) . (upper_bound A)) - ((tan (#) cosec) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: tan (#) cosec is_differentiable_on Z by A1, FDIFF_9:44; A4: for x being Real st x in dom ((tan (#) cosec) `| Z) holds ((tan (#) cosec) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((tan (#) cosec) `| Z) implies ((tan (#) cosec) `| Z) . x = f . x ) assume x in dom ((tan (#) cosec) `| Z) ; ::_thesis: ((tan (#) cosec) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((tan (#) cosec) `| Z) . x = ((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) by A1, FDIFF_9:44 .= f . x by A1, A5 ; hence ((tan (#) cosec) `| Z) . x = f . x ; ::_thesis: verum end; dom ((tan (#) cosec) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (tan (#) cosec) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((tan (#) cosec) . (upper_bound A)) - ((tan (#) cosec) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:47 for A being non empty closed_interval Subset of REAL for f 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 = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (cot (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot (#) cosec)) . (upper_bound A)) - ((- (cot (#) cosec)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (cot (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot (#) cosec)) . (upper_bound A)) - ((- (cot (#) cosec)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (cot (#) cosec) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot (#) cosec)) . (upper_bound A)) - ((- (cot (#) cosec)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (cot (#) cosec) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cot (#) cosec)) . (upper_bound A)) - ((- (cot (#) cosec)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) ) & Z c= dom (cot (#) cosec) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cot (#) cosec)) . (upper_bound A)) - ((- (cot (#) cosec)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (cot (#) cosec) is_differentiable_on Z by A1, Th13; A4: for x being Real st x in dom ((- (cot (#) cosec)) `| Z) holds ((- (cot (#) cosec)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (cot (#) cosec)) `| Z) implies ((- (cot (#) cosec)) `| Z) . x = f . x ) assume x in dom ((- (cot (#) cosec)) `| Z) ; ::_thesis: ((- (cot (#) cosec)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (cot (#) cosec)) `| Z) . x = ((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) by A1, Th13 .= f . x by A1, A5 ; hence ((- (cot (#) cosec)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (cot (#) cosec)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (cot (#) cosec)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (cot (#) cosec)) . (upper_bound A)) - ((- (cot (#) cosec)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:48 for A being non empty closed_interval Subset of REAL for f 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 = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (tan * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (tan * cot)) . (upper_bound A)) - ((- (tan * cot)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (tan * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (tan * cot)) . (upper_bound A)) - ((- (tan * cot)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (tan * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (tan * cot)) . (upper_bound A)) - ((- (tan * cot)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (tan * cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (tan * cot)) . (upper_bound A)) - ((- (tan * cot)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (tan * cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (tan * cot)) . (upper_bound A)) - ((- (tan * cot)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: Z c= dom (- (tan * cot)) by A1, VALUED_1:8; A4: tan * cot is_differentiable_on Z by A1, FDIFF_10:1; then A5: (- 1) (#) (tan * cot) is_differentiable_on Z by A3, FDIFF_1:20; A6: for x being Real st x in Z holds ((- (tan * cot)) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (tan * cot)) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) assume A7: x in Z ; ::_thesis: ((- (tan * cot)) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ((- (tan * cot)) `| Z) . x = ((- 1) (#) ((tan * cot) `| Z)) . x by A4, FDIFF_2:19 .= (- 1) * (((tan * cot) `| Z) . x) by VALUED_1:6 .= (- 1) * ((1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2)))) by A1, A7, FDIFF_10:1 .= (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ; hence ((- (tan * cot)) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ; ::_thesis: verum end; A8: for x being Real st x in dom ((- (tan * cot)) `| Z) holds ((- (tan * cot)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (tan * cot)) `| Z) implies ((- (tan * cot)) `| Z) . x = f . x ) assume x in dom ((- (tan * cot)) `| Z) ; ::_thesis: ((- (tan * cot)) `| Z) . x = f . x then A9: x in Z by A5, FDIFF_1:def_7; then ((- (tan * cot)) `| Z) . x = (1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) by A6 .= f . x by A1, A9 ; hence ((- (tan * cot)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (tan * cot)) `| Z) = dom f by A1, A5, FDIFF_1:def_7; then (- (tan * cot)) `| Z = f by A8, PARTFUN1:5; hence integral (f,A) = ((- (tan * cot)) . (upper_bound A)) - ((- (tan * cot)) . (lower_bound A)) by A1, A2, A5, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:49 for A being non empty closed_interval Subset of REAL for f 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 = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (tan * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan * tan) . (upper_bound A)) - ((tan * tan) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (tan * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan * tan) . (upper_bound A)) - ((tan * tan) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (tan * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan * tan) . (upper_bound A)) - ((tan * tan) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (tan * tan) & Z = dom f & f | A is continuous implies integral (f,A) = ((tan * tan) . (upper_bound A)) - ((tan * tan) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (tan * tan) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((tan * tan) . (upper_bound A)) - ((tan * tan) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: tan * tan is_differentiable_on Z by A1, FDIFF_10:2; A4: for x being Real st x in dom ((tan * tan) `| Z) holds ((tan * tan) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((tan * tan) `| Z) implies ((tan * tan) `| Z) . x = f . x ) assume x in dom ((tan * tan) `| Z) ; ::_thesis: ((tan * tan) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((tan * tan) `| Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) by A1, FDIFF_10:2 .= f . x by A1, A5 ; hence ((tan * tan) `| Z) . x = f . x ; ::_thesis: verum end; dom ((tan * tan) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (tan * tan) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((tan * tan) . (upper_bound A)) - ((tan * tan) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:50 for A being non empty closed_interval Subset of REAL for f 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 = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (cot * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((cot * cot) . (upper_bound A)) - ((cot * cot) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (cot * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((cot * cot) . (upper_bound A)) - ((cot * cot) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (cot * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((cot * cot) . (upper_bound A)) - ((cot * cot) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (cot * cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((cot * cot) . (upper_bound A)) - ((cot * cot) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) & Z c= dom (cot * cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((cot * cot) . (upper_bound A)) - ((cot * cot) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: cot * cot is_differentiable_on Z by A1, FDIFF_10:3; A4: for x being Real st x in dom ((cot * cot) `| Z) holds ((cot * cot) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((cot * cot) `| Z) implies ((cot * cot) `| Z) . x = f . x ) assume x in dom ((cot * cot) `| Z) ; ::_thesis: ((cot * cot) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((cot * cot) `| Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) by A1, FDIFF_10:3 .= f . x by A1, A5 ; hence ((cot * cot) `| Z) . x = f . x ; ::_thesis: verum end; dom ((cot * cot) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (cot * cot) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((cot * cot) . (upper_bound A)) - ((cot * cot) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:51 for A being non empty closed_interval Subset of REAL for f 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 = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (cot * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot * tan)) . (upper_bound A)) - ((- (cot * tan)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (cot * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot * tan)) . (upper_bound A)) - ((- (cot * tan)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (cot * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot * tan)) . (upper_bound A)) - ((- (cot * tan)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (cot * tan) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cot * tan)) . (upper_bound A)) - ((- (cot * tan)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) & Z c= dom (cot * tan) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cot * tan)) . (upper_bound A)) - ((- (cot * tan)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: Z c= dom (- (cot * tan)) by A1, VALUED_1:8; A4: cot * tan is_differentiable_on Z by A1, FDIFF_10:4; then A5: (- 1) (#) (cot * tan) is_differentiable_on Z by A3, FDIFF_1:20; A6: for x being Real st x in Z holds ((- (cot * tan)) `| Z) . x = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (cot * tan)) `| Z) . x = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) assume A7: x in Z ; ::_thesis: ((- (cot * tan)) `| Z) . x = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ((- (cot * tan)) `| Z) . x = ((- 1) (#) ((cot * tan) `| Z)) . x by A4, FDIFF_2:19 .= (- 1) * (((cot * tan) `| Z) . x) by VALUED_1:6 .= (- 1) * ((- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2))) by A1, A7, FDIFF_10:4 .= (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ; hence ((- (cot * tan)) `| Z) . x = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ; ::_thesis: verum end; A8: for x being Real st x in dom ((- (cot * tan)) `| Z) holds ((- (cot * tan)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (cot * tan)) `| Z) implies ((- (cot * tan)) `| Z) . x = f . x ) assume x in dom ((- (cot * tan)) `| Z) ; ::_thesis: ((- (cot * tan)) `| Z) . x = f . x then A9: x in Z by A5, FDIFF_1:def_7; then ((- (cot * tan)) `| Z) . x = (1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) by A6 .= f . x by A1, A9 ; hence ((- (cot * tan)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (cot * tan)) `| Z) = dom f by A1, A5, FDIFF_1:def_7; then (- (cot * tan)) `| Z = f by A8, PARTFUN1:5; hence integral (f,A) = ((- (cot * tan)) . (upper_bound A)) - ((- (cot * tan)) . (lower_bound A)) by A1, A2, A5, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:52 for A being non empty closed_interval Subset of REAL for f 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 = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) & Z c= dom (tan - cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan - cot) . (upper_bound A)) - ((tan - cot) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) & Z c= dom (tan - cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan - cot) . (upper_bound A)) - ((tan - cot) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) & Z c= dom (tan - cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan - cot) . (upper_bound A)) - ((tan - cot) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) & Z c= dom (tan - cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((tan - cot) . (upper_bound A)) - ((tan - cot) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) & Z c= dom (tan - cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((tan - cot) . (upper_bound A)) - ((tan - cot) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: tan - cot is_differentiable_on Z by A1, FDIFF_10:5; A4: for x being Real st x in dom ((tan - cot) `| Z) holds ((tan - cot) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((tan - cot) `| Z) implies ((tan - cot) `| Z) . x = f . x ) assume x in dom ((tan - cot) `| Z) ; ::_thesis: ((tan - cot) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((tan - cot) `| Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) by A1, FDIFF_10:5 .= f . x by A1, A5 ; hence ((tan - cot) `| Z) . x = f . x ; ::_thesis: verum end; dom ((tan - cot) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (tan - cot) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((tan - cot) . (upper_bound A)) - ((tan - cot) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:53 for A being non empty closed_interval Subset of REAL for f 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 = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) & Z c= dom (tan + cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan + cot) . (upper_bound A)) - ((tan + cot) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) & Z c= dom (tan + cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan + cot) . (upper_bound A)) - ((tan + cot) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) & Z c= dom (tan + cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan + cot) . (upper_bound A)) - ((tan + cot) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) & Z c= dom (tan + cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((tan + cot) . (upper_bound A)) - ((tan + cot) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) & Z c= dom (tan + cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((tan + cot) . (upper_bound A)) - ((tan + cot) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: tan + cot is_differentiable_on Z by A1, FDIFF_10:6; A4: for x being Real st x in dom ((tan + cot) `| Z) holds ((tan + cot) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((tan + cot) `| Z) implies ((tan + cot) `| Z) . x = f . x ) assume x in dom ((tan + cot) `| Z) ; ::_thesis: ((tan + cot) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((tan + cot) `| Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) by A1, FDIFF_10:6 .= f . x by A1, A5 ; hence ((tan + cot) `| Z) . x = f . x ; ::_thesis: verum end; dom ((tan + cot) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (tan + cot) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((tan + cot) . (upper_bound A)) - ((tan + cot) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:54 for A being non empty closed_interval Subset of REAL for f 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 = (cos . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((sin * sin) . (upper_bound A)) - ((sin * sin) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (cos . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((sin * sin) . (upper_bound A)) - ((sin * sin) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (cos . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((sin * sin) . (upper_bound A)) - ((sin * sin) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous implies integral (f,A) = ((sin * sin) . (upper_bound A)) - ((sin * sin) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((sin * sin) . (upper_bound A)) - ((sin * sin) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: sin * sin is_differentiable_on Z by FDIFF_10:7; A4: for x being Real st x in dom ((sin * sin) `| Z) holds ((sin * sin) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((sin * sin) `| Z) implies ((sin * sin) `| Z) . x = f . x ) assume x in dom ((sin * sin) `| Z) ; ::_thesis: ((sin * sin) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) by FDIFF_10:7 .= f . x by A1, A5 ; hence ((sin * sin) `| Z) . x = f . x ; ::_thesis: verum end; dom ((sin * sin) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (sin * sin) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((sin * sin) . (upper_bound A)) - ((sin * sin) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:55 for A being non empty closed_interval Subset of REAL for f 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 = (cos . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sin * cos)) . (upper_bound A)) - ((- (sin * cos)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (cos . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sin * cos)) . (upper_bound A)) - ((- (sin * cos)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (cos . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (sin * cos)) . (upper_bound A)) - ((- (sin * cos)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (sin * cos)) . (upper_bound A)) - ((- (sin * cos)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (sin * cos)) . (upper_bound A)) - ((- (sin * cos)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; ( dom cos = REAL & rng cos c= dom cos & dom sin = dom cos ) by SIN_COS:24; then dom (sin * cos) = REAL by RELAT_1:27; then A3: dom (- (sin * cos)) = REAL by VALUED_1:8; A4: sin * cos is_differentiable_on Z by FDIFF_10:8; then A5: (- 1) (#) (sin * cos) is_differentiable_on Z by A3, FDIFF_1:20; A6: for x being Real st x in Z holds ((- (sin * cos)) `| Z) . x = (cos . (cos . x)) * (sin . x) proof let x be Real; ::_thesis: ( x in Z implies ((- (sin * cos)) `| Z) . x = (cos . (cos . x)) * (sin . x) ) assume A7: x in Z ; ::_thesis: ((- (sin * cos)) `| Z) . x = (cos . (cos . x)) * (sin . x) ((- (sin * cos)) `| Z) . x = ((- 1) (#) ((sin * cos) `| Z)) . x by A4, FDIFF_2:19 .= (- 1) * (((sin * cos) `| Z) . x) by VALUED_1:6 .= (- 1) * (- ((cos . (cos . x)) * (sin . x))) by A7, FDIFF_10:8 .= (cos . (cos . x)) * (sin . x) ; hence ((- (sin * cos)) `| Z) . x = (cos . (cos . x)) * (sin . x) ; ::_thesis: verum end; A8: for x being Real st x in dom ((- (sin * cos)) `| Z) holds ((- (sin * cos)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (sin * cos)) `| Z) implies ((- (sin * cos)) `| Z) . x = f . x ) assume x in dom ((- (sin * cos)) `| Z) ; ::_thesis: ((- (sin * cos)) `| Z) . x = f . x then A9: x in Z by A5, FDIFF_1:def_7; then ((- (sin * cos)) `| Z) . x = (cos . (cos . x)) * (sin . x) by A6 .= f . x by A1, A9 ; hence ((- (sin * cos)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (sin * cos)) `| Z) = dom f by A1, A5, FDIFF_1:def_7; then (- (sin * cos)) `| Z = f by A8, PARTFUN1:5; hence integral (f,A) = ((- (sin * cos)) . (upper_bound A)) - ((- (sin * cos)) . (lower_bound A)) by A1, A2, A5, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:56 for A being non empty closed_interval Subset of REAL for f 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 = (sin . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cos * sin)) . (upper_bound A)) - ((- (cos * sin)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (sin . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cos * sin)) . (upper_bound A)) - ((- (cos * sin)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (sin . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cos * sin)) . (upper_bound A)) - ((- (cos * sin)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cos * sin)) . (upper_bound A)) - ((- (cos * sin)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . (sin . x)) * (cos . x) ) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cos * sin)) . (upper_bound A)) - ((- (cos * sin)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: dom sin = REAL by SIN_COS:24; ( rng sin c= dom sin & dom sin = dom cos ) by SIN_COS:24; then dom (cos * sin) = REAL by A3, RELAT_1:27; then A4: dom (- (cos * sin)) = REAL by VALUED_1:8; A5: cos * sin is_differentiable_on Z by FDIFF_10:9; then A6: (- 1) (#) (cos * sin) is_differentiable_on Z by A4, FDIFF_1:20; A7: for x being Real st x in Z holds ((- (cos * sin)) `| Z) . x = (sin . (sin . x)) * (cos . x) proof let x be Real; ::_thesis: ( x in Z implies ((- (cos * sin)) `| Z) . x = (sin . (sin . x)) * (cos . x) ) assume A8: x in Z ; ::_thesis: ((- (cos * sin)) `| Z) . x = (sin . (sin . x)) * (cos . x) ((- (cos * sin)) `| Z) . x = ((- 1) (#) ((cos * sin) `| Z)) . x by A5, FDIFF_2:19 .= (- 1) * (((cos * sin) `| Z) . x) by VALUED_1:6 .= (- 1) * (- ((sin . (sin . x)) * (cos . x))) by A8, FDIFF_10:9 .= (sin . (sin . x)) * (cos . x) ; hence ((- (cos * sin)) `| Z) . x = (sin . (sin . x)) * (cos . x) ; ::_thesis: verum end; A9: for x being Real st x in dom ((- (cos * sin)) `| Z) holds ((- (cos * sin)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (cos * sin)) `| Z) implies ((- (cos * sin)) `| Z) . x = f . x ) assume x in dom ((- (cos * sin)) `| Z) ; ::_thesis: ((- (cos * sin)) `| Z) . x = f . x then A10: x in Z by A6, FDIFF_1:def_7; then ((- (cos * sin)) `| Z) . x = (sin . (sin . x)) * (cos . x) by A7 .= f . x by A1, A10 ; hence ((- (cos * sin)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (cos * sin)) `| Z) = dom f by A1, A6, FDIFF_1:def_7; then (- (cos * sin)) `| Z = f by A9, PARTFUN1:5; hence integral (f,A) = ((- (cos * sin)) . (upper_bound A)) - ((- (cos * sin)) . (lower_bound A)) by A1, A2, A6, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:57 for A being non empty closed_interval Subset of REAL for f 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 = (sin . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((cos * cos) . (upper_bound A)) - ((cos * cos) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (sin . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((cos * cos) . (upper_bound A)) - ((cos * cos) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (sin . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((cos * cos) . (upper_bound A)) - ((cos * cos) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous implies integral (f,A) = ((cos * cos) . (upper_bound A)) - ((cos * cos) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . (cos . x)) * (sin . x) ) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((cos * cos) . (upper_bound A)) - ((cos * cos) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: cos * cos is_differentiable_on Z by FDIFF_10:10; A4: for x being Real st x in dom ((cos * cos) `| Z) holds ((cos * cos) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((cos * cos) `| Z) implies ((cos * cos) `| Z) . x = f . x ) assume x in dom ((cos * cos) `| Z) ; ::_thesis: ((cos * cos) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) by FDIFF_10:10 .= f . x by A1, A5 ; hence ((cos * cos) `| Z) . x = f . x ; ::_thesis: verum end; dom ((cos * cos) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (cos * cos) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((cos * cos) . (upper_bound A)) - ((cos * cos) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:58 for A being non empty closed_interval Subset of REAL for f 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 = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) & Z c= dom (cos (#) cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cos (#) cot)) . (upper_bound A)) - ((- (cos (#) cot)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) & Z c= dom (cos (#) cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cos (#) cot)) . (upper_bound A)) - ((- (cos (#) cot)) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) & Z c= dom (cos (#) cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cos (#) cot)) . (upper_bound A)) - ((- (cos (#) cot)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) & Z c= dom (cos (#) cot) & Z = dom f & f | A is continuous implies integral (f,A) = ((- (cos (#) cot)) . (upper_bound A)) - ((- (cos (#) cot)) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) ) & Z c= dom (cos (#) cot) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((- (cos (#) cot)) . (upper_bound A)) - ((- (cos (#) cot)) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: - (cos (#) cot) is_differentiable_on Z by A1, Th14; A4: for x being Real st x in dom ((- (cos (#) cot)) `| Z) holds ((- (cos (#) cot)) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- (cos (#) cot)) `| Z) implies ((- (cos (#) cot)) `| Z) . x = f . x ) assume x in dom ((- (cos (#) cot)) `| Z) ; ::_thesis: ((- (cos (#) cot)) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((- (cos (#) cot)) `| Z) . x = (cos . x) + ((cos . x) / ((sin . x) ^2)) by A1, Th14 .= f . x by A1, A5 ; hence ((- (cos (#) cot)) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- (cos (#) cot)) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (- (cos (#) cot)) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((- (cos (#) cot)) . (upper_bound A)) - ((- (cos (#) cot)) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGR14:59 for A being non empty closed_interval Subset of REAL for f 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 = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) & Z c= dom (sin (#) tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((sin (#) tan) . (upper_bound A)) - ((sin (#) tan) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f 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 = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) & Z c= dom (sin (#) tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((sin (#) tan) . (upper_bound A)) - ((sin (#) tan) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) & Z c= dom (sin (#) tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((sin (#) tan) . (upper_bound A)) - ((sin (#) tan) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) & Z c= dom (sin (#) tan) & Z = dom f & f | A is continuous implies integral (f,A) = ((sin (#) tan) . (upper_bound A)) - ((sin (#) tan) . (lower_bound A)) ) assume A1: ( A c= Z & ( for x being Real st x in Z holds f . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) & Z c= dom (sin (#) tan) & Z = dom f & f | A is continuous ) ; ::_thesis: integral (f,A) = ((sin (#) tan) . (upper_bound A)) - ((sin (#) tan) . (lower_bound A)) then A2: ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11; A3: sin (#) tan is_differentiable_on Z by A1, FDIFF_10:12; A4: for x being Real st x in dom ((sin (#) tan) `| Z) holds ((sin (#) tan) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((sin (#) tan) `| Z) implies ((sin (#) tan) `| Z) . x = f . x ) assume x in dom ((sin (#) tan) `| Z) ; ::_thesis: ((sin (#) tan) `| Z) . x = f . x then A5: x in Z by A3, FDIFF_1:def_7; then ((sin (#) tan) `| Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) by A1, FDIFF_10:12 .= f . x by A1, A5 ; hence ((sin (#) tan) `| Z) . x = f . x ; ::_thesis: verum end; dom ((sin (#) tan) `| Z) = dom f by A1, A3, FDIFF_1:def_7; then (sin (#) tan) `| Z = f by A4, PARTFUN1:5; hence integral (f,A) = ((sin (#) tan) . (upper_bound A)) - ((sin (#) tan) . (lower_bound A)) by A1, A2, A3, INTEGRA5:13; ::_thesis: verum end;