:: INTEGRA9 semantic presentation begin Lm1: dom (- (exp_R * (AffineMap ((- 1),0)))) = [#] REAL by FUNCT_2:def_1; theorem :: INTEGRA9:1 ( - (exp_R * (AffineMap ((- 1),0))) is_differentiable_on REAL & ( for x being Real holds ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ) ) proof A1: [#] REAL = dom (exp_R * (AffineMap ((- 1),0))) by FUNCT_2:def_1; A2: [#] REAL = dom (AffineMap ((- 1),0)) by FUNCT_2:def_1; A3: for x being Real st x in REAL holds (AffineMap ((- 1),0)) . x = ((- 1) * x) + 0 by FCONT_1:def_4; then A4: AffineMap ((- 1),0) is_differentiable_on REAL by A2, FDIFF_1:23; for x being Real st x in REAL holds exp_R * (AffineMap ((- 1),0)) is_differentiable_in x proof let x be Real; ::_thesis: ( x in REAL implies exp_R * (AffineMap ((- 1),0)) is_differentiable_in x ) assume x in REAL ; ::_thesis: exp_R * (AffineMap ((- 1),0)) is_differentiable_in x AffineMap ((- 1),0) is_differentiable_in x by A2, A4, FDIFF_1:9; hence exp_R * (AffineMap ((- 1),0)) is_differentiable_in x by TAYLOR_1:19; ::_thesis: verum end; then A5: exp_R * (AffineMap ((- 1),0)) is_differentiable_on REAL by A1, FDIFF_1:9; for x being Real st x in REAL holds ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) proof let x be Real; ::_thesis: ( x in REAL implies ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ) assume x in REAL ; ::_thesis: ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) A6: AffineMap ((- 1),0) is_differentiable_in x by A2, A4, FDIFF_1:9; ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = (- 1) * (diff ((exp_R * (AffineMap ((- 1),0))),x)) by A5, Lm1, FDIFF_1:20 .= (- 1) * ((exp_R . ((AffineMap ((- 1),0)) . x)) * (diff ((AffineMap ((- 1),0)),x))) by A6, TAYLOR_1:19 .= (- 1) * ((exp_R . ((AffineMap ((- 1),0)) . x)) * (((AffineMap ((- 1),0)) `| REAL) . x)) by A4, FDIFF_1:def_7 .= (- 1) * ((exp_R . ((AffineMap ((- 1),0)) . x)) * (- 1)) by A2, A3, FDIFF_1:23 .= (- 1) * ((exp_R . (((- 1) * x) + 0)) * (- 1)) by FCONT_1:def_4 .= exp_R (- x) ; hence ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ; ::_thesis: verum end; hence ( - (exp_R * (AffineMap ((- 1),0))) is_differentiable_on REAL & ( for x being Real holds ((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . x = exp_R (- x) ) ) by A5, Lm1, FDIFF_1:20; ::_thesis: verum end; theorem Th2: :: INTEGRA9:2 for r being Real st r <> 0 holds ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) ) proof let r be Real; ::_thesis: ( r <> 0 implies ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) ) ) A1: [#] REAL = dom (exp_R * (AffineMap (r,0))) by FUNCT_2:def_1; A2: [#] REAL = dom (AffineMap (r,0)) by FUNCT_2:def_1; A3: for x being Real st x in REAL holds (AffineMap (r,0)) . x = (r * x) + 0 by FCONT_1:def_4; then A4: AffineMap (r,0) is_differentiable_on REAL by A2, FDIFF_1:23; for x being Real st x in REAL holds exp_R * (AffineMap (r,0)) is_differentiable_in x proof let x be Real; ::_thesis: ( x in REAL implies exp_R * (AffineMap (r,0)) is_differentiable_in x ) assume x in REAL ; ::_thesis: exp_R * (AffineMap (r,0)) is_differentiable_in x AffineMap (r,0) is_differentiable_in x by A2, A4, FDIFF_1:9; hence exp_R * (AffineMap (r,0)) is_differentiable_in x by TAYLOR_1:19; ::_thesis: verum end; then A5: ( [#] REAL = dom ((1 / r) (#) (exp_R * (AffineMap (r,0)))) & exp_R * (AffineMap (r,0)) is_differentiable_on REAL ) by A1, FDIFF_1:9, FUNCT_2:def_1; assume A6: r <> 0 ; ::_thesis: ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) ) for x being Real st x in REAL holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x proof let x be Real; ::_thesis: ( x in REAL implies (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) assume x in REAL ; ::_thesis: (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x A7: AffineMap (r,0) is_differentiable_in x by A2, A4, FDIFF_1:9; (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (1 / r) * (diff ((exp_R * (AffineMap (r,0))),x)) by A5, FDIFF_1:20 .= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (diff ((AffineMap (r,0)),x))) by A7, TAYLOR_1:19 .= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (((AffineMap (r,0)) `| REAL) . x)) by A4, FDIFF_1:def_7 .= (1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * r) by A2, A3, FDIFF_1:23 .= (r * (1 / r)) * (exp_R . ((AffineMap (r,0)) . x)) .= (r / r) * (exp_R . ((AffineMap (r,0)) . x)) by XCMPLX_1:99 .= 1 * (exp_R . ((AffineMap (r,0)) . x)) by A6, XCMPLX_1:60 .= (exp_R * (AffineMap (r,0))) . x by A1, FUNCT_1:12 ; hence (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ; ::_thesis: verum end; hence ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) ) by A5, FDIFF_1:20; ::_thesis: verum end; theorem :: INTEGRA9:3 for r being Real for A being non empty closed_interval Subset of REAL st r <> 0 holds integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A)) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL st r <> 0 holds integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: ( r <> 0 implies integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A)) ) A1: dom (exp_R * (AffineMap (r,0))) = REAL by FUNCT_2:def_1; A2: (AffineMap (r,0)) | A is continuous ; assume A3: r <> 0 ; ::_thesis: integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A)) then (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL by Th2; then A4: dom (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) = dom (exp_R * (AffineMap (r,0))) by A1, FDIFF_1:def_7; exp_R | REAL is continuous by FDIFF_1:25, SIN_COS:66; then A5: exp_R | ((AffineMap (r,0)) .: A) is continuous by FCONT_1:16; then (exp_R * (AffineMap (r,0))) | A is continuous by A2, FCONT_1:25; then A6: exp_R * (AffineMap (r,0)) is_integrable_on A by A1, INTEGRA5:11; for x being Real st x in dom (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x by A3, Th2; then A7: ((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL = exp_R * (AffineMap (r,0)) by A4, PARTFUN1:5; (exp_R * (AffineMap (r,0))) | A is bounded by A1, A2, A5, FCONT_1:25, INTEGRA5:10; hence integral ((exp_R * (AffineMap (r,0))),A) = (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (upper_bound A)) - (((1 / r) (#) (exp_R * (AffineMap (r,0)))) . (lower_bound A)) by A3, A6, A7, Th2, INTEGRA5:13; ::_thesis: verum end; theorem Th4: :: INTEGRA9:4 for n being Element of NAT st n <> 0 holds ( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) ) proof let n be Element of NAT ; ::_thesis: ( n <> 0 implies ( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) ) ) A1: [#] REAL = dom ((- (1 / n)) (#) (cos * (AffineMap (n,0)))) by FUNCT_2:def_1; A2: ( [#] REAL = dom (cos * (AffineMap (n,0))) & ( for x being Real st x in REAL holds (AffineMap (n,0)) . x = (n * x) + 0 ) ) by FCONT_1:def_4, FUNCT_2:def_1; then A3: cos * (AffineMap (n,0)) is_differentiable_on REAL by FDIFF_4:38; assume A4: n <> 0 ; ::_thesis: ( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) ) for x being Real st x in REAL holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) proof let x be Real; ::_thesis: ( x in REAL implies (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) assume x in REAL ; ::_thesis: (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (- (1 / n)) * (diff ((cos * (AffineMap (n,0))),x)) by A1, A3, FDIFF_1:20 .= (- (1 / n)) * (((cos * (AffineMap (n,0))) `| REAL) . x) by A3, FDIFF_1:def_7 .= (- (1 / n)) * (- (n * (sin . ((n * x) + 0)))) by A2, FDIFF_4:38 .= ((1 / n) * n) * (sin . ((n * x) + 0)) .= (n / n) * (sin . ((n * x) + 0)) by XCMPLX_1:99 .= 1 * (sin . ((n * x) + 0)) by A4, XCMPLX_1:60 .= sin (n * x) ; hence (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ; ::_thesis: verum end; hence ( (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) ) ) by A1, A3, FDIFF_1:20; ::_thesis: verum end; theorem :: INTEGRA9:5 for n being Element of NAT for A being non empty closed_interval Subset of REAL st n <> 0 holds integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A)) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st n <> 0 holds integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: ( n <> 0 implies integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A)) ) assume A1: n <> 0 ; ::_thesis: integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A)) A2: [#] REAL = dom (sin * (AffineMap (n,0))) by FUNCT_2:def_1; A3: for x being Real st x in REAL holds (AffineMap (n,0)) . x = n * x proof let x be Real; ::_thesis: ( x in REAL implies (AffineMap (n,0)) . x = n * x ) assume x in REAL ; ::_thesis: (AffineMap (n,0)) . x = n * x (AffineMap (n,0)) . x = (n * x) + 0 by FCONT_1:def_4 .= n * x ; hence (AffineMap (n,0)) . x = n * x ; ::_thesis: verum end; A4: for x being Real st x in dom (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) holds (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (sin * (AffineMap (n,0))) . x proof let x be Real; ::_thesis: ( x in dom (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) implies (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (sin * (AffineMap (n,0))) . x ) assume x in dom (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) ; ::_thesis: (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (sin * (AffineMap (n,0))) . x (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = sin (n * x) by A1, Th4 .= sin . ((AffineMap (n,0)) . x) by A3 .= (sin * (AffineMap (n,0))) . x by A2, FUNCT_1:12 ; hence (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (sin * (AffineMap (n,0))) . x ; ::_thesis: verum end; (- (1 / n)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL by A1, Th4; then dom (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL) = dom (sin * (AffineMap (n,0))) by A2, FDIFF_1:def_7; then A5: ((- (1 / n)) (#) (cos * (AffineMap (n,0)))) `| REAL = sin * (AffineMap (n,0)) by A4, PARTFUN1:5; A6: (AffineMap (n,0)) | A is continuous ; sin | REAL is continuous by FDIFF_1:25, SIN_COS:68; then A7: sin | ((AffineMap (n,0)) .: A) is continuous by FCONT_1:16; then (sin * (AffineMap (n,0))) | A is continuous by A6, FCONT_1:25; then A8: sin * (AffineMap (n,0)) is_integrable_on A by A2, INTEGRA5:11; (sin * (AffineMap (n,0))) | A is bounded by A2, A6, A7, FCONT_1:25, INTEGRA5:10; hence integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A)) by A1, A8, A5, Th4, INTEGRA5:13; ::_thesis: verum end; theorem Th6: :: INTEGRA9:6 for n being Element of NAT st n <> 0 holds ( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) ) proof let n be Element of NAT ; ::_thesis: ( n <> 0 implies ( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) ) ) A1: [#] REAL = dom ((1 / n) (#) (sin * (AffineMap (n,0)))) by FUNCT_2:def_1; A2: ( [#] REAL = dom (sin * (AffineMap (n,0))) & ( for x being Real st x in REAL holds (AffineMap (n,0)) . x = (n * x) + 0 ) ) by FCONT_1:def_4, FUNCT_2:def_1; then A3: sin * (AffineMap (n,0)) is_differentiable_on REAL by FDIFF_4:37; assume A4: n <> 0 ; ::_thesis: ( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) ) for x being Real st x in REAL holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) proof let x be Real; ::_thesis: ( x in REAL implies (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) assume x in REAL ; ::_thesis: (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (1 / n) * (diff ((sin * (AffineMap (n,0))),x)) by A1, A3, FDIFF_1:20 .= (1 / n) * (((sin * (AffineMap (n,0))) `| REAL) . x) by A3, FDIFF_1:def_7 .= (1 / n) * (n * (cos . ((n * x) + 0))) by A2, FDIFF_4:37 .= (n * (1 / n)) * (cos . ((n * x) + 0)) .= (n / n) * (cos . ((n * x) + 0)) by XCMPLX_1:99 .= 1 * (cos . ((n * x) + 0)) by A4, XCMPLX_1:60 .= cos (n * x) ; hence (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ; ::_thesis: verum end; hence ( (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) ) ) by A1, A3, FDIFF_1:20; ::_thesis: verum end; theorem :: INTEGRA9:7 for n being Element of NAT for A being non empty closed_interval Subset of REAL st n <> 0 holds integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A)) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st n <> 0 holds integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: ( n <> 0 implies integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A)) ) assume A1: n <> 0 ; ::_thesis: integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A)) A2: [#] REAL = dom (cos * (AffineMap (n,0))) by FUNCT_2:def_1; A3: for x being Real st x in REAL holds (AffineMap (n,0)) . x = n * x proof let x be Real; ::_thesis: ( x in REAL implies (AffineMap (n,0)) . x = n * x ) assume x in REAL ; ::_thesis: (AffineMap (n,0)) . x = n * x (AffineMap (n,0)) . x = (n * x) + 0 by FCONT_1:def_4 .= n * x ; hence (AffineMap (n,0)) . x = n * x ; ::_thesis: verum end; A4: for x being Real st x in dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) holds (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x proof let x be Real; ::_thesis: ( x in dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) implies (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x ) assume x in dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) ; ::_thesis: (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = cos (n * x) by A1, Th6 .= cos . ((AffineMap (n,0)) . x) by A3 .= (cos * (AffineMap (n,0))) . x by A2, FUNCT_1:12 ; hence (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x ; ::_thesis: verum end; (1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL by A1, Th6; then dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) = dom (cos * (AffineMap (n,0))) by A2, FDIFF_1:def_7; then A5: ((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL = cos * (AffineMap (n,0)) by A4, PARTFUN1:5; A6: (AffineMap (n,0)) | A is continuous ; cos | REAL is continuous by FDIFF_1:25, SIN_COS:67; then A7: cos | ((AffineMap (n,0)) .: A) is continuous by FCONT_1:16; then (cos * (AffineMap (n,0))) | A is continuous by A6, FCONT_1:25; then A8: cos * (AffineMap (n,0)) is_integrable_on A by A2, INTEGRA5:11; (cos * (AffineMap (n,0))) | A is bounded by A2, A6, A7, FCONT_1:25, INTEGRA5:10; hence integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A)) by A1, A8, A5, Th6, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:8 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z holds integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (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 holds integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) ) assume A1: A c= Z ; ::_thesis: integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) A2: dom (- (id Z)) = dom (id Z) by VALUED_1:8; A3: dom (((- (id Z)) (#) cos) + sin) = (dom ((- (id Z)) (#) cos)) /\ REAL by SIN_COS:24, VALUED_1:def_1 .= dom ((- (id Z)) (#) cos) by XBOOLE_1:28 .= (dom (- (id Z))) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (- (id Z)) by XBOOLE_1:28 .= Z by A2, RELAT_1:45 ; then A4: ((- (id Z)) (#) cos) + sin is_differentiable_on Z by FDIFF_4:46; A5: for x being Real st x in Z holds ((id Z) (#) sin) . x = x * (sin . x) proof let x be Real; ::_thesis: ( x in Z implies ((id Z) (#) sin) . x = x * (sin . x) ) assume A6: x in Z ; ::_thesis: ((id Z) (#) sin) . x = x * (sin . x) ((id Z) (#) sin) . x = ((id Z) . x) * (sin . x) by VALUED_1:5 .= x * (sin . x) by A6, FUNCT_1:18 ; hence ((id Z) (#) sin) . x = x * (sin . x) ; ::_thesis: verum end; A7: for x being Real st x in dom ((((- (id Z)) (#) cos) + sin) `| Z) holds ((((- (id Z)) (#) cos) + sin) `| Z) . x = ((id Z) (#) sin) . x proof let x be Real; ::_thesis: ( x in dom ((((- (id Z)) (#) cos) + sin) `| Z) implies ((((- (id Z)) (#) cos) + sin) `| Z) . x = ((id Z) (#) sin) . x ) assume x in dom ((((- (id Z)) (#) cos) + sin) `| Z) ; ::_thesis: ((((- (id Z)) (#) cos) + sin) `| Z) . x = ((id Z) (#) sin) . x then A8: x in Z by A4, FDIFF_1:def_7; then ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) by A3, FDIFF_4:46 .= ((id Z) (#) sin) . x by A5, A8 ; hence ((((- (id Z)) (#) cos) + sin) `| Z) . x = ((id Z) (#) sin) . x ; ::_thesis: verum end; A9: dom ((id Z) (#) sin) = (dom (id Z)) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (id Z) by XBOOLE_1:28 .= Z by RELAT_1:45 ; then dom ((((- (id Z)) (#) cos) + sin) `| Z) = dom ((id Z) (#) sin) by A4, FDIFF_1:def_7; then A10: (((- (id Z)) (#) cos) + sin) `| Z = (id Z) (#) sin by A7, PARTFUN1:5; A11: ((id Z) (#) sin) | Z is continuous by A9, FDIFF_1:25, FDIFF_4:45; then ((id Z) (#) sin) | A is continuous by A1, FCONT_1:16; then A12: (id Z) (#) sin is_integrable_on A by A1, A9, INTEGRA5:11; ((id Z) (#) sin) | A is bounded by A1, A9, A11, FCONT_1:16, INTEGRA5:10; hence integral (((id Z) (#) sin),A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) by A1, A3, A12, A10, FDIFF_4:46, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:9 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z holds integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (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 holds integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A)) ) assume A1: A c= Z ; ::_thesis: integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A)) A2: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; A3: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; dom (((id Z) (#) sin) + cos) = (dom ((id Z) (#) sin)) /\ REAL by SIN_COS:24, VALUED_1:def_1 .= dom ((id Z) (#) sin) by XBOOLE_1:28 .= (dom (id Z)) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (id Z) by XBOOLE_1:28 ; then A4: dom (((id Z) (#) sin) + cos) = Z by RELAT_1:45; then A5: ((id Z) (#) sin) + cos is_differentiable_on Z by FDIFF_4:47; A6: for x being Real st x in Z holds ((id Z) (#) cos) . x = x * (cos . x) proof let x be Real; ::_thesis: ( x in Z implies ((id Z) (#) cos) . x = x * (cos . x) ) assume A7: x in Z ; ::_thesis: ((id Z) (#) cos) . x = x * (cos . x) ((id Z) (#) cos) . x = ((id Z) . x) * (cos . x) by VALUED_1:5 .= x * (cos . x) by A7, FUNCT_1:18 ; hence ((id Z) (#) cos) . x = x * (cos . x) ; ::_thesis: verum end; A8: for x being Real st x in dom ((((id Z) (#) sin) + cos) `| Z) holds ((((id Z) (#) sin) + cos) `| Z) . x = ((id Z) (#) cos) . x proof let x be Real; ::_thesis: ( x in dom ((((id Z) (#) sin) + cos) `| Z) implies ((((id Z) (#) sin) + cos) `| Z) . x = ((id Z) (#) cos) . x ) assume x in dom ((((id Z) (#) sin) + cos) `| Z) ; ::_thesis: ((((id Z) (#) sin) + cos) `| Z) . x = ((id Z) (#) cos) . x then A9: x in Z by A5, FDIFF_1:def_7; then ((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) by A4, FDIFF_4:47 .= ((id Z) (#) cos) . x by A6, A9 ; hence ((((id Z) (#) sin) + cos) `| Z) . x = ((id Z) (#) cos) . x ; ::_thesis: verum end; A10: dom ((id Z) (#) cos) = (dom (id Z)) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (id Z) by XBOOLE_1:28 .= Z by RELAT_1:45 ; then dom ((((id Z) (#) sin) + cos) `| Z) = dom ((id Z) (#) cos) by A5, FDIFF_1:def_7; then A11: (((id Z) (#) sin) + cos) `| Z = (id Z) (#) cos by A8, PARTFUN1:5; Z = (dom (id Z)) /\ (dom cos) by A10, VALUED_1:def_4; then Z c= dom (id Z) by XBOOLE_1:18; then id Z is_differentiable_on Z by A3, FDIFF_1:23; then A12: ((id Z) (#) cos) | Z is continuous by A10, A2, FDIFF_1:21, FDIFF_1:25; then ((id Z) (#) cos) | A is continuous by A1, FCONT_1:16; then A13: (id Z) (#) cos is_integrable_on A by A1, A10, INTEGRA5:11; ((id Z) (#) cos) | A is bounded by A1, A10, A12, FCONT_1:16, INTEGRA5:10; hence integral (((id Z) (#) cos),A) = ((((id Z) (#) sin) + cos) . (upper_bound A)) - ((((id Z) (#) sin) + cos) . (lower_bound A)) by A1, A4, A13, A11, FDIFF_4:47, INTEGRA5:13; ::_thesis: verum end; theorem Th10: :: INTEGRA9:10 for Z being open Subset of REAL holds ( (id Z) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( (id Z) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) ) ) A1: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; A2: dom ((id Z) (#) cos) = (dom (id Z)) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (id Z) by XBOOLE_1:28 .= Z by RELAT_1:45 ; then Z c= (dom (id Z)) /\ (dom cos) by VALUED_1:def_4; then A3: Z c= dom (id Z) by XBOOLE_1:18; for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; then A4: id Z is_differentiable_on Z by A3, FDIFF_1:23; A5: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((id_Z)_(#)_cos)_`|_Z)_._x_=_(cos_._x)_-_(x_*_(sin_._x)) let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) ) assume A6: x in Z ; ::_thesis: (((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) hence (((id Z) (#) cos) `| Z) . x = ((cos . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff (cos,x))) by A2, A4, A1, FDIFF_1:21 .= ((cos . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff (cos,x))) by A4, A6, FDIFF_1:def_7 .= ((cos . x) * 1) + (((id Z) . x) * (diff (cos,x))) by A3, A5, A6, FDIFF_1:23 .= ((cos . x) * 1) + (((id Z) . x) * (- (sin . x))) by SIN_COS:63 .= (cos . x) + (x * (- (sin . x))) by A6, FUNCT_1:18 .= (cos . x) - (x * (sin . x)) ; ::_thesis: verum end; hence ( (id Z) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) cos) `| Z) . x = (cos . x) - (x * (sin . x)) ) ) by A2, A4, A1, FDIFF_1:21; ::_thesis: verum end; Lm2: for x being Real holds ( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) ) proof let x be Real; ::_thesis: ( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) ) A1: sin is_differentiable_in x by SIN_COS:64; then diff ((- sin),x) = - (diff (sin,x)) by INTEGRA8:22 .= - (cos . x) by SIN_COS:64 ; hence ( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) ) by A1, INTEGRA8:22; ::_thesis: verum end; theorem Th11: :: INTEGRA9:11 for Z being open Subset of REAL holds ( (- sin) + ((id Z) (#) cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( (- sin) + ((id Z) (#) cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) ) ) dom ((- sin) + ((id Z) (#) cos)) = (dom (- sin)) /\ (dom ((id Z) (#) cos)) by VALUED_1:def_1 .= REAL /\ (dom ((id Z) (#) cos)) by SIN_COS:24, VALUED_1:8 .= dom ((id Z) (#) cos) by XBOOLE_1:28 .= (dom (id Z)) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (id Z) by XBOOLE_1:28 ; then A1: Z = dom ((- sin) + ((id Z) (#) cos)) by RELAT_1:45; A2: (id Z) (#) cos is_differentiable_on Z by Th10; A3: - sin is_differentiable_on Z by FDIFF_1:26, INTEGRA8:24; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((-_sin)_+_((id_Z)_(#)_cos))_`|_Z)_._x_=_-_(x_*_(sin_._x)) let x be Real; ::_thesis: ( x in Z implies (((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) ) assume A4: x in Z ; ::_thesis: (((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) hence (((- sin) + ((id Z) (#) cos)) `| Z) . x = (diff ((- sin),x)) + (diff (((id Z) (#) cos),x)) by A1, A2, A3, FDIFF_1:18 .= ((((id Z) (#) cos) `| Z) . x) + (diff ((- sin),x)) by A2, A4, FDIFF_1:def_7 .= ((cos . x) - (x * (sin . x))) + (diff ((- sin),x)) by A4, Th10 .= ((cos . x) - (x * (sin . x))) + (- (cos . x)) by Lm2 .= - (x * (sin . x)) ; ::_thesis: verum end; hence ( (- sin) + ((id Z) (#) cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) ) ) by A1, A2, A3, FDIFF_1:18; ::_thesis: verum end; theorem :: INTEGRA9:12 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z holds integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (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 holds integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A)) ) assume A1: A c= Z ; ::_thesis: integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A)) A2: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; A3: (- sin) + ((id Z) (#) cos) is_differentiable_on Z by Th11; A4: for x being Real st x in Z holds (- (id Z)) . x = ((- 1) * x) + 0 proof let x be Real; ::_thesis: ( x in Z implies (- (id Z)) . x = ((- 1) * x) + 0 ) assume A5: x in Z ; ::_thesis: (- (id Z)) . x = ((- 1) * x) + 0 (- (id Z)) . x = - ((id Z) . x) by VALUED_1:8 .= - x by A5, FUNCT_1:18 .= ((- 1) * x) + 0 ; hence (- (id Z)) . x = ((- 1) * x) + 0 ; ::_thesis: verum end; A6: for x being Real st x in Z holds ((- (id Z)) (#) sin) . x = - (x * (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((- (id Z)) (#) sin) . x = - (x * (sin . x)) ) assume A7: x in Z ; ::_thesis: ((- (id Z)) (#) sin) . x = - (x * (sin . x)) ((- (id Z)) (#) sin) . x = ((- (id Z)) . x) * (sin . x) by VALUED_1:5 .= (((- 1) * x) + 0) * (sin . x) by A4, A7 .= - (x * (sin . x)) ; hence ((- (id Z)) (#) sin) . x = - (x * (sin . x)) ; ::_thesis: verum end; A8: for x being Real st x in dom (((- sin) + ((id Z) (#) cos)) `| Z) holds (((- sin) + ((id Z) (#) cos)) `| Z) . x = ((- (id Z)) (#) sin) . x proof let x be Real; ::_thesis: ( x in dom (((- sin) + ((id Z) (#) cos)) `| Z) implies (((- sin) + ((id Z) (#) cos)) `| Z) . x = ((- (id Z)) (#) sin) . x ) assume x in dom (((- sin) + ((id Z) (#) cos)) `| Z) ; ::_thesis: (((- sin) + ((id Z) (#) cos)) `| Z) . x = ((- (id Z)) (#) sin) . x then A9: x in Z by A3, FDIFF_1:def_7; then (((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x)) by Th11 .= ((- (id Z)) (#) sin) . x by A6, A9 ; hence (((- sin) + ((id Z) (#) cos)) `| Z) . x = ((- (id Z)) (#) sin) . x ; ::_thesis: verum end; dom ((- (id Z)) (#) sin) = (dom (- (id Z))) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (- (id Z)) by XBOOLE_1:28 .= dom (id Z) by VALUED_1:8 ; then A10: Z = dom ((- (id Z)) (#) sin) by RELAT_1:45; then dom (((- sin) + ((id Z) (#) cos)) `| Z) = dom ((- (id Z)) (#) sin) by A3, FDIFF_1:def_7; then A11: ((- sin) + ((id Z) (#) cos)) `| Z = (- (id Z)) (#) sin by A8, PARTFUN1:5; Z c= (dom (- (id Z))) /\ (dom sin) by A10, VALUED_1:def_4; then Z c= dom (- (id Z)) by XBOOLE_1:18; then - (id Z) is_differentiable_on Z by A4, FDIFF_1:23; then A12: ((- (id Z)) (#) sin) | Z is continuous by A10, A2, FDIFF_1:21, FDIFF_1:25; then ((- (id Z)) (#) sin) | A is continuous by A1, FCONT_1:16; then A13: (- (id Z)) (#) sin is_integrable_on A by A1, A10, INTEGRA5:11; ((- (id Z)) (#) sin) | A is bounded by A1, A10, A12, FCONT_1:16, INTEGRA5:10; hence integral (((- (id Z)) (#) sin),A) = (((- sin) + ((id Z) (#) cos)) . (upper_bound A)) - (((- sin) + ((id Z) (#) cos)) . (lower_bound A)) by A1, A13, A11, Th11, INTEGRA5:13; ::_thesis: verum end; theorem Th13: :: INTEGRA9:13 for Z being open Subset of REAL holds ( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) ) dom ((- cos) - ((id Z) (#) sin)) = (dom (- cos)) /\ (dom ((id Z) (#) sin)) by VALUED_1:12 .= REAL /\ (dom ((id Z) (#) sin)) by SIN_COS:24, VALUED_1:8 .= dom ((id Z) (#) sin) by XBOOLE_1:28 .= (dom (id Z)) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (id Z) by XBOOLE_1:28 ; then A1: Z = dom ((- cos) - ((id Z) (#) sin)) by RELAT_1:45; then Z c= (dom (- cos)) /\ (dom ((id Z) (#) sin)) by VALUED_1:12; then A2: Z c= dom ((id Z) (#) sin) by XBOOLE_1:18; then A3: (id Z) (#) sin is_differentiable_on Z by FDIFF_4:45; A4: - cos is_differentiable_on Z by FDIFF_1:26, INTEGRA8:26; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((-_cos)_-_((id_Z)_(#)_sin))_`|_Z)_._x_=_-_(x_*_(cos_._x)) let x be Real; ::_thesis: ( x in Z implies (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) assume A5: x in Z ; ::_thesis: (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) hence (((- cos) - ((id Z) (#) sin)) `| Z) . x = (diff ((- cos),x)) - (diff (((id Z) (#) sin),x)) by A1, A3, A4, FDIFF_1:19 .= (sin . x) - (diff (((id Z) (#) sin),x)) by INTEGRA8:26 .= (sin . x) - ((((id Z) (#) sin) `| Z) . x) by A3, A5, FDIFF_1:def_7 .= (sin . x) - ((sin . x) + (x * (cos . x))) by A2, A5, FDIFF_4:45 .= - (x * (cos . x)) ; ::_thesis: verum end; hence ( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) ) by A1, A3, A4, FDIFF_1:19; ::_thesis: verum end; theorem :: INTEGRA9:14 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z holds integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (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 holds integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A)) ) assume A1: A c= Z ; ::_thesis: integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A)) A2: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; A3: (- cos) - ((id Z) (#) sin) is_differentiable_on Z by Th13; A4: for x being Real st x in Z holds (- (id Z)) . x = ((- 1) * x) + 0 proof let x be Real; ::_thesis: ( x in Z implies (- (id Z)) . x = ((- 1) * x) + 0 ) assume A5: x in Z ; ::_thesis: (- (id Z)) . x = ((- 1) * x) + 0 (- (id Z)) . x = - ((id Z) . x) by VALUED_1:8 .= - x by A5, FUNCT_1:18 .= ((- 1) * x) + 0 ; hence (- (id Z)) . x = ((- 1) * x) + 0 ; ::_thesis: verum end; A6: for x being Real st x in Z holds ((- (id Z)) (#) cos) . x = - (x * (cos . x)) proof let x be Real; ::_thesis: ( x in Z implies ((- (id Z)) (#) cos) . x = - (x * (cos . x)) ) assume A7: x in Z ; ::_thesis: ((- (id Z)) (#) cos) . x = - (x * (cos . x)) ((- (id Z)) (#) cos) . x = ((- (id Z)) . x) * (cos . x) by VALUED_1:5 .= (((- 1) * x) + 0) * (cos . x) by A4, A7 .= - (x * (cos . x)) ; hence ((- (id Z)) (#) cos) . x = - (x * (cos . x)) ; ::_thesis: verum end; A8: for x being Real st x in dom (((- cos) - ((id Z) (#) sin)) `| Z) holds (((- cos) - ((id Z) (#) sin)) `| Z) . x = ((- (id Z)) (#) cos) . x proof let x be Real; ::_thesis: ( x in dom (((- cos) - ((id Z) (#) sin)) `| Z) implies (((- cos) - ((id Z) (#) sin)) `| Z) . x = ((- (id Z)) (#) cos) . x ) assume x in dom (((- cos) - ((id Z) (#) sin)) `| Z) ; ::_thesis: (((- cos) - ((id Z) (#) sin)) `| Z) . x = ((- (id Z)) (#) cos) . x then A9: x in Z by A3, FDIFF_1:def_7; then (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) by Th13 .= ((- (id Z)) (#) cos) . x by A6, A9 ; hence (((- cos) - ((id Z) (#) sin)) `| Z) . x = ((- (id Z)) (#) cos) . x ; ::_thesis: verum end; dom ((- (id Z)) (#) cos) = (dom (- (id Z))) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (- (id Z)) by XBOOLE_1:28 .= dom (id Z) by VALUED_1:8 ; then A10: Z = dom ((- (id Z)) (#) cos) by RELAT_1:45; then dom (((- cos) - ((id Z) (#) sin)) `| Z) = dom ((- (id Z)) (#) cos) by A3, FDIFF_1:def_7; then A11: ((- cos) - ((id Z) (#) sin)) `| Z = (- (id Z)) (#) cos by A8, PARTFUN1:5; Z = (dom (- (id Z))) /\ (dom cos) by A10, VALUED_1:def_4; then Z c= dom (- (id Z)) by XBOOLE_1:18; then - (id Z) is_differentiable_on Z by A4, FDIFF_1:23; then A12: ((- (id Z)) (#) cos) | Z is continuous by A10, A2, FDIFF_1:21, FDIFF_1:25; then ((- (id Z)) (#) cos) | A is continuous by A1, FCONT_1:16; then A13: (- (id Z)) (#) cos is_integrable_on A by A1, A10, INTEGRA5:11; ((- (id Z)) (#) cos) | A is bounded by A1, A10, A12, FCONT_1:16, INTEGRA5:10; hence integral (((- (id Z)) (#) cos),A) = (((- cos) - ((id Z) (#) sin)) . (upper_bound A)) - (((- cos) - ((id Z) (#) sin)) . (lower_bound A)) by A1, A13, A11, Th13, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:15 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z holds integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (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 holds integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A)) ) assume A1: A c= Z ; ::_thesis: integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A)) A2: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; A3: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; dom (sin + ((id Z) (#) cos)) = REAL /\ (dom ((id Z) (#) cos)) by SIN_COS:24, VALUED_1:def_1 .= dom ((id Z) (#) cos) by XBOOLE_1:28 .= (dom (id Z)) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (id Z) by XBOOLE_1:28 ; then A4: Z = dom (sin + ((id Z) (#) cos)) by RELAT_1:45; then Z = (dom sin) /\ (dom ((id Z) (#) cos)) by VALUED_1:def_1; then A5: Z c= dom ((id Z) (#) cos) by XBOOLE_1:18; then Z c= (dom (id Z)) /\ (dom cos) by VALUED_1:def_4; then Z c= dom (id Z) by XBOOLE_1:18; then id Z is_differentiable_on Z by A3, FDIFF_1:23; then ( sin is_differentiable_on Z & (id Z) (#) cos is_differentiable_on Z ) by A5, A2, FDIFF_1:21, FDIFF_1:26, SIN_COS:68; then A6: (sin + ((id Z) (#) cos)) | Z is continuous by A4, FDIFF_1:18, FDIFF_1:25; then (sin + ((id Z) (#) cos)) | A is continuous by A1, FCONT_1:16; then A7: sin + ((id Z) (#) cos) is_integrable_on A by A1, A4, INTEGRA5:11; A8: dom ((id Z) (#) sin) = (dom (id Z)) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (id Z) by XBOOLE_1:28 .= Z by RELAT_1:45 ; then A9: (id Z) (#) sin is_differentiable_on Z by FDIFF_4:45; A10: for x being Real st x in Z holds (sin + ((id Z) (#) cos)) . x = (sin . x) + (x * (cos . x)) proof let x be Real; ::_thesis: ( x in Z implies (sin + ((id Z) (#) cos)) . x = (sin . x) + (x * (cos . x)) ) assume A11: x in Z ; ::_thesis: (sin + ((id Z) (#) cos)) . x = (sin . x) + (x * (cos . x)) then (sin + ((id Z) (#) cos)) . x = (sin . x) + (((id Z) (#) cos) . x) by A4, VALUED_1:def_1 .= (sin . x) + (((id Z) . x) * (cos . x)) by VALUED_1:5 .= (sin . x) + (x * (cos . x)) by A11, FUNCT_1:18 ; hence (sin + ((id Z) (#) cos)) . x = (sin . x) + (x * (cos . x)) ; ::_thesis: verum end; A12: for x being Real st x in dom (((id Z) (#) sin) `| Z) holds (((id Z) (#) sin) `| Z) . x = (sin + ((id Z) (#) cos)) . x proof let x be Real; ::_thesis: ( x in dom (((id Z) (#) sin) `| Z) implies (((id Z) (#) sin) `| Z) . x = (sin + ((id Z) (#) cos)) . x ) assume x in dom (((id Z) (#) sin) `| Z) ; ::_thesis: (((id Z) (#) sin) `| Z) . x = (sin + ((id Z) (#) cos)) . x then A13: x in Z by A9, FDIFF_1:def_7; then (((id Z) (#) sin) `| Z) . x = (sin . x) + (x * (cos . x)) by A8, FDIFF_4:45 .= (sin + ((id Z) (#) cos)) . x by A10, A13 ; hence (((id Z) (#) sin) `| Z) . x = (sin + ((id Z) (#) cos)) . x ; ::_thesis: verum end; dom (((id Z) (#) sin) `| Z) = dom (sin + ((id Z) (#) cos)) by A4, A9, FDIFF_1:def_7; then A14: ((id Z) (#) sin) `| Z = sin + ((id Z) (#) cos) by A12, PARTFUN1:5; (sin + ((id Z) (#) cos)) | A is bounded by A1, A4, A6, FCONT_1:16, INTEGRA5:10; hence integral ((sin + ((id Z) (#) cos)),A) = (((id Z) (#) sin) . (upper_bound A)) - (((id Z) (#) sin) . (lower_bound A)) by A1, A8, A7, A14, FDIFF_4:45, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:16 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z holds integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (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 holds integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z implies integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A)) ) assume A1: A c= Z ; ::_thesis: integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A)) A2: - cos is_differentiable_on Z by FDIFF_1:26, INTEGRA8:26; A3: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; A4: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; dom ((- cos) + ((id Z) (#) sin)) = (dom (- cos)) /\ (dom ((id Z) (#) sin)) by VALUED_1:def_1 .= REAL /\ (dom ((id Z) (#) sin)) by SIN_COS:24, VALUED_1:8 .= dom ((id Z) (#) sin) by XBOOLE_1:28 .= (dom (id Z)) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (id Z) by XBOOLE_1:28 ; then A5: Z = dom ((- cos) + ((id Z) (#) sin)) by RELAT_1:45; then Z = (dom (- cos)) /\ (dom ((id Z) (#) sin)) by VALUED_1:def_1; then A6: Z c= dom ((id Z) (#) sin) by XBOOLE_1:18; then Z c= (dom (id Z)) /\ (dom sin) by VALUED_1:def_4; then Z c= dom (id Z) by XBOOLE_1:18; then id Z is_differentiable_on Z by A4, FDIFF_1:23; then (id Z) (#) sin is_differentiable_on Z by A6, A3, FDIFF_1:21; then A7: ((- cos) + ((id Z) (#) sin)) | Z is continuous by A5, A2, FDIFF_1:18, FDIFF_1:25; then ((- cos) + ((id Z) (#) sin)) | A is continuous by A1, FCONT_1:16; then A8: (- cos) + ((id Z) (#) sin) is_integrable_on A by A1, A5, INTEGRA5:11; dom ((- (id Z)) (#) cos) = (dom (- (id Z))) /\ REAL by SIN_COS:24, VALUED_1:def_4 .= dom (- (id Z)) by XBOOLE_1:28 .= dom (id Z) by VALUED_1:8 ; then A9: dom ((- (id Z)) (#) cos) = Z by RELAT_1:45; then A10: (- (id Z)) (#) cos is_differentiable_on Z by FDIFF_4:44; A11: for x being Real st x in Z holds ((- cos) + ((id Z) (#) sin)) . x = (- (cos . x)) + (x * (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies ((- cos) + ((id Z) (#) sin)) . x = (- (cos . x)) + (x * (sin . x)) ) assume A12: x in Z ; ::_thesis: ((- cos) + ((id Z) (#) sin)) . x = (- (cos . x)) + (x * (sin . x)) then ((- cos) + ((id Z) (#) sin)) . x = ((- cos) . x) + (((id Z) (#) sin) . x) by A5, VALUED_1:def_1 .= ((- cos) . x) + (((id Z) . x) * (sin . x)) by VALUED_1:5 .= ((- cos) . x) + (x * (sin . x)) by A12, FUNCT_1:18 .= (- (cos . x)) + (x * (sin . x)) by VALUED_1:8 ; hence ((- cos) + ((id Z) (#) sin)) . x = (- (cos . x)) + (x * (sin . x)) ; ::_thesis: verum end; A13: for x being Real st x in dom (((- (id Z)) (#) cos) `| Z) holds (((- (id Z)) (#) cos) `| Z) . x = ((- cos) + ((id Z) (#) sin)) . x proof let x be Real; ::_thesis: ( x in dom (((- (id Z)) (#) cos) `| Z) implies (((- (id Z)) (#) cos) `| Z) . x = ((- cos) + ((id Z) (#) sin)) . x ) assume x in dom (((- (id Z)) (#) cos) `| Z) ; ::_thesis: (((- (id Z)) (#) cos) `| Z) . x = ((- cos) + ((id Z) (#) sin)) . x then A14: x in Z by A10, FDIFF_1:def_7; then (((- (id Z)) (#) cos) `| Z) . x = (- (cos . x)) + (x * (sin . x)) by A9, FDIFF_4:44 .= ((- cos) + ((id Z) (#) sin)) . x by A11, A14 ; hence (((- (id Z)) (#) cos) `| Z) . x = ((- cos) + ((id Z) (#) sin)) . x ; ::_thesis: verum end; dom (((- (id Z)) (#) cos) `| Z) = dom ((- cos) + ((id Z) (#) sin)) by A5, A10, FDIFF_1:def_7; then A15: ((- (id Z)) (#) cos) `| Z = (- cos) + ((id Z) (#) sin) by A13, PARTFUN1:5; ((- cos) + ((id Z) (#) sin)) | A is bounded by A1, A5, A7, FCONT_1:16, INTEGRA5:10; hence integral (((- cos) + ((id Z) (#) sin)),A) = (((- (id Z)) (#) cos) . (upper_bound A)) - (((- (id Z)) (#) cos) . (lower_bound A)) by A1, A9, A8, A15, FDIFF_4:44, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:17 for A being non empty closed_interval Subset of REAL holds integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A)) A1: for x being Real st x in REAL holds (AffineMap (1,(- 1))) . x = x - 1 proof let x be Real; ::_thesis: ( x in REAL implies (AffineMap (1,(- 1))) . x = x - 1 ) assume x in REAL ; ::_thesis: (AffineMap (1,(- 1))) . x = x - 1 (AffineMap (1,(- 1))) . x = (1 * x) + (- 1) by FCONT_1:def_4 .= x - 1 ; hence (AffineMap (1,(- 1))) . x = x - 1 ; ::_thesis: verum end; A2: dom (exp_R (#) (AffineMap (1,(- 1)))) = [#] REAL by FUNCT_2:def_1; A3: for x being Real st x in REAL holds ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x) proof let x be Real; ::_thesis: ( x in REAL implies ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x) ) assume x in REAL ; ::_thesis: ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x) ((AffineMap (1,0)) (#) exp_R) . x = ((AffineMap (1,0)) . x) * (exp_R . x) by VALUED_1:5 .= ((1 * x) + 0) * (exp_R . x) by FCONT_1:def_4 .= x * (exp_R . x) ; hence ((AffineMap (1,0)) (#) exp_R) . x = x * (exp_R . x) ; ::_thesis: verum end; A4: for x being Real st x in dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) holds ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x proof let x be Real; ::_thesis: ( x in dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) implies ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x ) assume x in dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) ; ::_thesis: ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = x * (exp_R . x) by A2, A1, FDIFF_4:55 .= ((AffineMap (1,0)) (#) exp_R) . x by A3 ; hence ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . x = ((AffineMap (1,0)) (#) exp_R) . x ; ::_thesis: verum end; A5: [#] REAL = dom ((AffineMap (1,0)) (#) exp_R) by FUNCT_2:def_1; ( dom (AffineMap (1,0)) = [#] REAL & ( for x being Real st x in REAL holds (AffineMap (1,0)) . x = (1 * x) + 0 ) ) by FCONT_1:def_4, FUNCT_2:def_1; then AffineMap (1,0) is_differentiable_on REAL by FDIFF_1:23; then (AffineMap (1,0)) (#) exp_R is_differentiable_on REAL by A5, FDIFF_1:21, TAYLOR_1:16; then A6: ((AffineMap (1,0)) (#) exp_R) | REAL is continuous by FDIFF_1:25; then ((AffineMap (1,0)) (#) exp_R) | A is continuous by FCONT_1:16; then A7: (AffineMap (1,0)) (#) exp_R is_integrable_on A by A5, INTEGRA5:11; exp_R (#) (AffineMap (1,(- 1))) is_differentiable_on REAL by A2, A1, FDIFF_4:55; then dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) = dom ((AffineMap (1,0)) (#) exp_R) by A5, FDIFF_1:def_7; then A8: (exp_R (#) (AffineMap (1,(- 1)))) `| REAL = (AffineMap (1,0)) (#) exp_R by A4, PARTFUN1:5; ((AffineMap (1,0)) (#) exp_R) | A is bounded by A5, A6, FCONT_1:16, INTEGRA5:10; hence integral (((AffineMap (1,0)) (#) exp_R),A) = ((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A)) by A2, A1, A7, A8, FDIFF_4:55, INTEGRA5:13; ::_thesis: verum end; theorem Th18: :: INTEGRA9:18 for n being Element of NAT holds ( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ) ) proof let n be Element of NAT ; ::_thesis: ( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ) ) A1: [#] REAL = dom ((1 / (n + 1)) (#) (#Z (n + 1))) by FUNCT_2:def_1; ( [#] REAL = dom (#Z (n + 1)) & ( for x being Real st x in REAL holds #Z (n + 1) is_differentiable_in x ) ) by FUNCT_2:def_1, TAYLOR_1:2; then A2: #Z (n + 1) is_differentiable_on REAL by FDIFF_1:9; A3: for x being Real st x in REAL holds ((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n) proof set m = n + 1; let x be Real; ::_thesis: ( x in REAL implies ((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n) ) assume x in REAL ; ::_thesis: ((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n) diff ((#Z (n + 1)),x) = (n + 1) * (x #Z ((n + 1) - 1)) by TAYLOR_1:2; hence ((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n) by A2, FDIFF_1:def_7; ::_thesis: verum end; for x being Real st x in REAL holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n proof let x be Real; ::_thesis: ( x in REAL implies (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ) assume x in REAL ; ::_thesis: (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = (1 / (n + 1)) * (diff ((#Z (n + 1)),x)) by A1, A2, FDIFF_1:20 .= (1 / (n + 1)) * (((#Z (n + 1)) `| REAL) . x) by A2, FDIFF_1:def_7 .= (1 / (n + 1)) * ((n + 1) * (x #Z n)) by A3 .= ((1 / (n + 1)) * (n + 1)) * (x #Z n) .= ((n + 1) / (n + 1)) * (x #Z n) by XCMPLX_1:99 .= 1 * (x #Z n) by XCMPLX_1:60 ; hence (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ; ::_thesis: verum end; hence ( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ) ) by A1, A2, FDIFF_1:20; ::_thesis: verum end; theorem :: INTEGRA9:19 for n being Element of NAT for A being non empty closed_interval Subset of REAL holds integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1))) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL holds integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1))) let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1))) A1: dom (#Z n) = [#] REAL by FUNCT_2:def_1; A2: for x being Real st x in dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = (#Z n) . x proof let x be Real; ::_thesis: ( x in dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) implies (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = (#Z n) . x ) assume x in dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) ; ::_thesis: (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = (#Z n) . x (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n by Th18 .= (#Z n) . x by TAYLOR_1:def_1 ; hence (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = (#Z n) . x ; ::_thesis: verum end; ( dom (#Z (n + 1)) = [#] REAL & ( for x being Real st x in REAL holds #Z (n + 1) is_differentiable_in x ) ) by FUNCT_2:def_1, TAYLOR_1:2; then ( [#] REAL = dom ((1 / (n + 1)) (#) (#Z (n + 1))) & #Z (n + 1) is_differentiable_on REAL ) by FDIFF_1:9, FUNCT_2:def_1; then (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL by FDIFF_1:20; then dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) = dom (#Z n) by A1, FDIFF_1:def_7; then A3: ((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL = #Z n by A2, PARTFUN1:5; A4: (#Z (n + 1)) . (upper_bound A) = (upper_bound A) #Z (n + 1) by TAYLOR_1:def_1 .= (upper_bound A) |^ (n + 1) by PREPOWER:36 ; for x being Real st x in REAL holds #Z n is_differentiable_in x by TAYLOR_1:2; then #Z n is_differentiable_on REAL by A1, FDIFF_1:9; then A5: (#Z n) | REAL is continuous by FDIFF_1:25; then (#Z n) | A is continuous by FCONT_1:16; then A6: #Z n is_integrable_on A by A1, INTEGRA5:11; A7: (#Z (n + 1)) . (lower_bound A) = (lower_bound A) #Z (n + 1) by TAYLOR_1:def_1 .= (lower_bound A) |^ (n + 1) by PREPOWER:36 ; (#Z n) | A is bounded by A1, A5, FCONT_1:16, INTEGRA5:10; then integral ((#Z n),A) = (((1 / (n + 1)) (#) (#Z (n + 1))) . (upper_bound A)) - (((1 / (n + 1)) (#) (#Z (n + 1))) . (lower_bound A)) by A6, A3, Th18, INTEGRA5:13 .= ((1 / (n + 1)) * ((#Z (n + 1)) . (upper_bound A))) - (((1 / (n + 1)) (#) (#Z (n + 1))) . (lower_bound A)) by VALUED_1:6 .= ((1 / (n + 1)) * ((#Z (n + 1)) . (upper_bound A))) - ((1 / (n + 1)) * ((#Z (n + 1)) . (lower_bound A))) by VALUED_1:6 .= ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1))) by A4, A7 ; hence integral ((#Z n),A) = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1))) ; ::_thesis: verum end; begin theorem Th20: :: INTEGRA9:20 for f, g being PartFunc of REAL,REAL for C being non empty Subset of REAL holds (f - g) || C = (f || C) - (g || C) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for C being non empty Subset of REAL holds (f - g) || C = (f || C) - (g || C) let C be non empty Subset of REAL; ::_thesis: (f - g) || C = (f || C) - (g || C) A1: dom ((f || C) - (g || C)) = (dom (f | C)) /\ (dom (g | C)) by VALUED_1:12 .= ((dom f) /\ C) /\ (dom (g | C)) by RELAT_1:61 .= ((dom f) /\ C) /\ ((dom g) /\ C) by RELAT_1:61 .= (dom f) /\ (C /\ ((dom g) /\ C)) by XBOOLE_1:16 .= (dom f) /\ ((dom g) /\ (C /\ C)) by XBOOLE_1:16 .= (dom f) /\ ((dom g) /\ C) ; A2: dom ((f - g) || C) = (dom (f - g)) /\ C by RELAT_1:61 .= ((dom f) /\ (dom g)) /\ C by VALUED_1:12 ; then A3: dom ((f - g) || C) = dom ((f || C) - (g || C)) by A1, XBOOLE_1:16; for c being Element of C st c in dom ((f - g) || C) holds ((f - g) || C) . c = ((f || C) - (g || C)) . c proof let c be Element of C; ::_thesis: ( c in dom ((f - g) || C) implies ((f - g) || C) . c = ((f || C) - (g || C)) . c ) assume A4: c in dom ((f - g) || C) ; ::_thesis: ((f - g) || C) . c = ((f || C) - (g || C)) . c then c in (dom (f - g)) /\ C by RELAT_1:61; then A5: c in dom (f - g) by XBOOLE_0:def_4; A6: c in (dom (f || C)) /\ (dom (g || C)) by A3, A4, VALUED_1:12; then A7: c in dom (f | C) by XBOOLE_0:def_4; A8: ((f - g) || C) . c = (f - g) . c by A4, FUNCT_1:47 .= (f . c) - (g . c) by A5, VALUED_1:13 ; A9: c in dom (g | C) by A6, XBOOLE_0:def_4; ((f || C) - (g || C)) . c = ((f || C) . c) - ((g || C) . c) by A3, A4, VALUED_1:13 .= (f . c) - ((g | C) . c) by A7, FUNCT_1:47 ; hence ((f - g) || C) . c = ((f || C) - (g || C)) . c by A8, A9, FUNCT_1:47; ::_thesis: verum end; hence (f - g) || C = (f || C) - (g || C) by A2, A1, PARTFUN1:5, XBOOLE_1:16; ::_thesis: verum end; theorem Th21: :: INTEGRA9:21 for f1, f2, g being PartFunc of REAL,REAL for C being non empty Subset of REAL holds ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C proof let f1, f2, g be PartFunc of REAL,REAL; ::_thesis: for C being non empty Subset of REAL holds ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C let C be non empty Subset of REAL; ::_thesis: ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C A1: dom (((f1 (#) g) + (f2 (#) g)) || C) = (dom ((f1 (#) g) + (f2 (#) g))) /\ C by RELAT_1:61 .= ((dom (f1 (#) g)) /\ (dom (f2 (#) g))) /\ C by VALUED_1:def_1 .= (((dom f1) /\ (dom g)) /\ (dom (f2 (#) g))) /\ C by VALUED_1:def_4 .= (((dom f1) /\ (dom g)) /\ ((dom f2) /\ (dom g))) /\ C by VALUED_1:def_4 .= ((dom f1) /\ (((dom g) /\ (dom f2)) /\ (dom g))) /\ C by XBOOLE_1:16 .= ((dom f1) /\ ((dom f2) /\ ((dom g) /\ (dom g)))) /\ C by XBOOLE_1:16 .= (((dom f1) /\ (dom f2)) /\ (dom g)) /\ C by XBOOLE_1:16 ; A2: dom (((f1 + f2) || C) (#) (g || C)) = (dom ((f1 + f2) || C)) /\ (dom (g || C)) by VALUED_1:def_4 .= ((dom (f1 + f2)) /\ C) /\ (dom (g | C)) by RELAT_1:61 .= ((dom (f1 + f2)) /\ C) /\ ((dom g) /\ C) by RELAT_1:61 .= (((dom f1) /\ (dom f2)) /\ C) /\ ((dom g) /\ C) by VALUED_1:def_1 .= ((dom f1) /\ (dom f2)) /\ ((C /\ (dom g)) /\ C) by XBOOLE_1:16 .= ((dom f1) /\ (dom f2)) /\ ((dom g) /\ (C /\ C)) by XBOOLE_1:16 .= (((dom f1) /\ (dom f2)) /\ (dom g)) /\ C by XBOOLE_1:16 ; for c being Element of C st c in dom (((f1 + f2) || C) (#) (g || C)) holds (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c proof let c be Element of C; ::_thesis: ( c in dom (((f1 + f2) || C) (#) (g || C)) implies (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c ) assume A3: c in dom (((f1 + f2) || C) (#) (g || C)) ; ::_thesis: (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c then A4: c in (dom ((f1 + f2) || C)) /\ (dom (g || C)) by VALUED_1:def_4; then A5: c in dom (g | C) by XBOOLE_0:def_4; c in (dom ((f1 (#) g) + (f2 (#) g))) /\ C by A2, A1, A3, RELAT_1:61; then A6: c in dom ((f1 (#) g) + (f2 (#) g)) by XBOOLE_0:def_4; then A7: c in (dom (f1 (#) g)) /\ (dom (f2 (#) g)) by VALUED_1:def_1; then A8: c in dom (f1 (#) g) by XBOOLE_0:def_4; A9: c in dom ((f1 + f2) | C) by A4, XBOOLE_0:def_4; then c in (dom (f1 + f2)) /\ C by RELAT_1:61; then A10: c in dom (f1 + f2) by XBOOLE_0:def_4; A11: (((f1 + f2) || C) (#) (g || C)) . c = (((f1 + f2) || C) . c) * ((g || C) . c) by A3, VALUED_1:def_4 .= ((f1 + f2) . c) * ((g | C) . c) by A9, FUNCT_1:47 .= ((f1 . c) + (f2 . c)) * ((g | C) . c) by A10, VALUED_1:def_1 ; A12: c in dom (f2 (#) g) by A7, XBOOLE_0:def_4; (((f1 (#) g) + (f2 (#) g)) || C) . c = ((f1 (#) g) + (f2 (#) g)) . c by A2, A1, A3, FUNCT_1:47 .= ((f1 (#) g) . c) + ((f2 (#) g) . c) by A6, VALUED_1:def_1 .= ((f1 . c) * (g . c)) + ((f2 (#) g) . c) by A8, VALUED_1:def_4 .= ((f1 . c) * (g . c)) + ((f2 . c) * (g . c)) by A12, VALUED_1:def_4 .= ((f1 . c) + (f2 . c)) * (g . c) ; hence (((f1 + f2) || C) (#) (g || C)) . c = (((f1 (#) g) + (f2 (#) g)) || C) . c by A5, A11, FUNCT_1:47; ::_thesis: verum end; hence ((f1 + f2) || C) (#) (g || C) = ((f1 (#) g) + (f2 (#) g)) || C by A2, A1, PARTFUN1:5; ::_thesis: verum end; theorem Th22: :: INTEGRA9:22 for f1, f2, g being PartFunc of REAL,REAL for C being non empty Subset of REAL holds ((f1 - f2) || C) (#) (g || C) = ((f1 (#) g) - (f2 (#) g)) || C proof let f1, f2, g be PartFunc of REAL,REAL; ::_thesis: for C being non empty Subset of REAL holds ((f1 - f2) || C) (#) (g || C) = ((f1 (#) g) - (f2 (#) g)) || C let C be non empty Subset of REAL; ::_thesis: ((f1 - f2) || C) (#) (g || C) = ((f1 (#) g) - (f2 (#) g)) || C A1: dom (((f1 (#) g) - (f2 (#) g)) || C) = (dom ((f1 (#) g) - (f2 (#) g))) /\ C by RELAT_1:61 .= ((dom (f1 (#) g)) /\ (dom (f2 (#) g))) /\ C by VALUED_1:12 .= (((dom f1) /\ (dom g)) /\ (dom (f2 (#) g))) /\ C by VALUED_1:def_4 .= (((dom f1) /\ (dom g)) /\ ((dom f2) /\ (dom g))) /\ C by VALUED_1:def_4 .= ((dom f1) /\ (((dom g) /\ (dom f2)) /\ (dom g))) /\ C by XBOOLE_1:16 .= ((dom f1) /\ ((dom f2) /\ ((dom g) /\ (dom g)))) /\ C by XBOOLE_1:16 .= (((dom f1) /\ (dom f2)) /\ (dom g)) /\ C by XBOOLE_1:16 ; A2: dom (((f1 - f2) || C) (#) (g || C)) = (dom ((f1 - f2) | C)) /\ (dom (g | C)) by VALUED_1:def_4 .= ((dom (f1 - f2)) /\ C) /\ (dom (g | C)) by RELAT_1:61 .= ((dom (f1 - f2)) /\ C) /\ ((dom g) /\ C) by RELAT_1:61 .= (((dom f1) /\ (dom f2)) /\ C) /\ ((dom g) /\ C) by VALUED_1:12 .= ((dom f1) /\ (dom f2)) /\ ((C /\ (dom g)) /\ C) by XBOOLE_1:16 .= ((dom f1) /\ (dom f2)) /\ ((dom g) /\ (C /\ C)) by XBOOLE_1:16 .= (((dom f1) /\ (dom f2)) /\ (dom g)) /\ C by XBOOLE_1:16 ; for c being Element of C st c in dom (((f1 - f2) || C) (#) (g || C)) holds (((f1 - f2) || C) (#) (g || C)) . c = (((f1 (#) g) - (f2 (#) g)) || C) . c proof let c be Element of C; ::_thesis: ( c in dom (((f1 - f2) || C) (#) (g || C)) implies (((f1 - f2) || C) (#) (g || C)) . c = (((f1 (#) g) - (f2 (#) g)) || C) . c ) assume A3: c in dom (((f1 - f2) || C) (#) (g || C)) ; ::_thesis: (((f1 - f2) || C) (#) (g || C)) . c = (((f1 (#) g) - (f2 (#) g)) || C) . c then A4: c in (dom ((f1 - f2) || C)) /\ (dom (g || C)) by VALUED_1:def_4; then A5: c in dom (g | C) by XBOOLE_0:def_4; c in (dom ((f1 (#) g) - (f2 (#) g))) /\ C by A2, A1, A3, RELAT_1:61; then A6: c in dom ((f1 (#) g) - (f2 (#) g)) by XBOOLE_0:def_4; then A7: c in (dom (f1 (#) g)) /\ (dom (f2 (#) g)) by VALUED_1:12; then A8: c in dom (f1 (#) g) by XBOOLE_0:def_4; A9: c in dom ((f1 - f2) | C) by A4, XBOOLE_0:def_4; then c in (dom (f1 - f2)) /\ C by RELAT_1:61; then A10: c in dom (f1 - f2) by XBOOLE_0:def_4; A11: (((f1 - f2) || C) (#) (g || C)) . c = (((f1 - f2) | C) . c) * ((g | C) . c) by A3, VALUED_1:def_4 .= ((f1 - f2) . c) * ((g | C) . c) by A9, FUNCT_1:47 .= ((f1 . c) - (f2 . c)) * ((g | C) . c) by A10, VALUED_1:13 ; A12: c in dom (f2 (#) g) by A7, XBOOLE_0:def_4; (((f1 (#) g) - (f2 (#) g)) || C) . c = ((f1 (#) g) - (f2 (#) g)) . c by A2, A1, A3, FUNCT_1:47 .= ((f1 (#) g) . c) - ((f2 (#) g) . c) by A6, VALUED_1:13 .= ((f1 . c) * (g . c)) - ((f2 (#) g) . c) by A8, VALUED_1:def_4 .= ((f1 . c) * (g . c)) - ((f2 . c) * (g . c)) by A12, VALUED_1:def_4 .= ((f1 . c) - (f2 . c)) * (g . c) ; hence (((f1 - f2) || C) (#) (g || C)) . c = (((f1 (#) g) - (f2 (#) g)) || C) . c by A5, A11, FUNCT_1:47; ::_thesis: verum end; hence ((f1 - f2) || C) (#) (g || C) = ((f1 (#) g) - (f2 (#) g)) || C by A2, A1, PARTFUN1:5; ::_thesis: verum end; theorem :: INTEGRA9:23 for f1, f2, g being PartFunc of REAL,REAL for C being non empty Subset of REAL holds ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C) proof let f1, f2, g be PartFunc of REAL,REAL; ::_thesis: for C being non empty Subset of REAL holds ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C) let C be non empty Subset of REAL; ::_thesis: ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C) ( ((f1 (#) f2) || C) (#) (g || C) = ((f1 || C) (#) (f2 || C)) (#) (g || C) & (f1 || C) (#) ((f2 (#) g) || C) = (f1 || C) (#) ((f2 || C) (#) (g || C)) ) by INTEGRA5:4; hence ((f1 (#) f2) || C) (#) (g || C) = (f1 || C) (#) ((f2 (#) g) || C) by RFUNCT_1:9; ::_thesis: verum end; definition let A be non empty closed_interval Subset of REAL; let f, g be PartFunc of REAL,REAL; func|||(f,g,A)||| -> Real equals :: INTEGRA9:def 1 integral ((f (#) g),A); correctness coherence integral ((f (#) g),A) is Real; ; end; :: deftheorem defines |||( INTEGRA9:def_1_:_ for A being non empty closed_interval Subset of REAL for f, g being PartFunc of REAL,REAL holds |||(f,g,A)||| = integral ((f (#) g),A); theorem :: INTEGRA9:24 for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL holds |||(f,g,A)||| = |||(g,f,A)||| ; theorem :: INTEGRA9:25 for f1, f2, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable holds |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| proof let f1, f2, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable holds |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable implies |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| ) assume A1: ( (f1 (#) g) || A is total & (f2 (#) g) || A is total ) ; ::_thesis: ( not ((f1 (#) g) || A) | A is bounded or not (f1 (#) g) || A is integrable or not ((f2 (#) g) || A) | A is bounded or not (f2 (#) g) || A is integrable or |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| ) assume A2: ( ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable ) ; ::_thesis: |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| |||((f1 + f2),g,A)||| = integral (((f1 + f2) || A) (#) (g || A)) by INTEGRA5:4 .= integral (((f1 (#) g) + (f2 (#) g)) || A) by Th21 .= integral (((f1 (#) g) || A) + ((f2 (#) g) || A)) by INTEGRA5:5 .= (integral ((f1 (#) g) || A)) + (integral ((f2 (#) g) || A)) by A1, A2, INTEGRA1:57 ; hence |||((f1 + f2),g,A)||| = |||(f1,g,A)||| + |||(f2,g,A)||| ; ::_thesis: verum end; theorem :: INTEGRA9:26 for f1, f2, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable holds |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| proof let f1, f2, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable holds |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f1 (#) g) || A is total & (f2 (#) g) || A is total & ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable implies |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| ) assume A1: ( (f1 (#) g) || A is total & (f2 (#) g) || A is total ) ; ::_thesis: ( not ((f1 (#) g) || A) | A is bounded or not (f1 (#) g) || A is integrable or not ((f2 (#) g) || A) | A is bounded or not (f2 (#) g) || A is integrable or |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| ) assume A2: ( ((f1 (#) g) || A) | A is bounded & (f1 (#) g) || A is integrable & ((f2 (#) g) || A) | A is bounded & (f2 (#) g) || A is integrable ) ; ::_thesis: |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| |||((f1 - f2),g,A)||| = integral (((f1 - f2) || A) (#) (g || A)) by INTEGRA5:4 .= integral (((f1 (#) g) - (f2 (#) g)) || A) by Th22 .= integral (((f1 (#) g) || A) - ((f2 (#) g) || A)) by Th20 .= (integral ((f1 (#) g) || A)) - (integral ((f2 (#) g) || A)) by A1, A2, INTEGRA2:33 ; hence |||((f1 - f2),g,A)||| = |||(f1,g,A)||| - |||(f2,g,A)||| ; ::_thesis: verum end; theorem :: INTEGRA9:27 for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds |||((- f),g,A)||| = - |||(f,g,A)||| proof let f, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds |||((- f),g,A)||| = - |||(f,g,A)||| let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) implies |||((- f),g,A)||| = - |||(f,g,A)||| ) assume A1: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) ) ; ::_thesis: |||((- f),g,A)||| = - |||(f,g,A)||| |||((- f),g,A)||| = integral (((- 1) (#) (f (#) g)),A) by RFUNCT_1:12 .= (- 1) * (integral ((f (#) g),A)) by A1, INTEGRA6:9 .= - |||(f,g,A)||| ; hence |||((- f),g,A)||| = - |||(f,g,A)||| ; ::_thesis: verum end; theorem :: INTEGRA9:28 for r being Real for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds |||((r (#) f),g,A)||| = r * |||(f,g,A)||| proof let r be Real; ::_thesis: for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds |||((r (#) f),g,A)||| = r * |||(f,g,A)||| let f, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds |||((r (#) f),g,A)||| = r * |||(f,g,A)||| let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) implies |||((r (#) f),g,A)||| = r * |||(f,g,A)||| ) assume A1: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) ) ; ::_thesis: |||((r (#) f),g,A)||| = r * |||(f,g,A)||| |||((r (#) f),g,A)||| = integral ((r (#) (f (#) g)),A) by RFUNCT_1:12 .= r * (integral ((f (#) g),A)) by A1, INTEGRA6:9 ; hence |||((r (#) f),g,A)||| = r * |||(f,g,A)||| ; ::_thesis: verum end; theorem :: INTEGRA9:29 for r, p being Real for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| proof let r, p be Real; ::_thesis: for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| let f, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) holds |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) implies |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| ) assume A1: ( (f (#) g) | A is bounded & f (#) g is_integrable_on A & A c= dom (f (#) g) ) ; ::_thesis: |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| |||((r (#) f),(p (#) g),A)||| = integral ((r (#) (f (#) (p (#) g))),A) by RFUNCT_1:12 .= integral ((r (#) (p (#) (f (#) g))),A) by RFUNCT_1:13 .= integral (((r * p) (#) (f (#) g)),A) by RFUNCT_1:17 .= (r * p) * (integral ((f (#) g),A)) by A1, INTEGRA6:9 ; hence |||((r (#) f),(p (#) g),A)||| = (r * p) * |||(f,g,A)||| ; ::_thesis: verum end; theorem :: INTEGRA9:30 for f, g, h being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL holds |||((f (#) g),h,A)||| = |||(f,(g (#) h),A)||| by RFUNCT_1:9; theorem Th31: :: INTEGRA9:31 for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A holds |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| proof let f, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A holds |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A implies |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| ) assume that A1: (f (#) f) || A is total and A2: (f (#) g) || A is total and A3: (g (#) g) || A is total ; ::_thesis: ( not ((f (#) f) || A) | A is bounded or not ((f (#) g) || A) | A is bounded or not ((g (#) g) || A) | A is bounded or not f (#) f is_integrable_on A or not f (#) g is_integrable_on A or not g (#) g is_integrable_on A or |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| ) assume that A4: ((f (#) f) || A) | A is bounded and A5: ((f (#) g) || A) | A is bounded and A6: ((g (#) g) || A) | A is bounded ; ::_thesis: ( not f (#) f is_integrable_on A or not f (#) g is_integrable_on A or not g (#) g is_integrable_on A or |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| ) assume that A7: f (#) f is_integrable_on A and A8: f (#) g is_integrable_on A and A9: g (#) g is_integrable_on A ; ::_thesis: |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| A10: (f (#) g) || A is integrable by A8, INTEGRA5:def_1; A11: (g (#) g) || A is integrable by A9, INTEGRA5:def_1; then A12: ((f (#) g) || A) + ((g (#) g) || A) is integrable by A2, A3, A5, A6, A10, INTEGRA1:57; A13: (f (#) f) || A is integrable by A7, INTEGRA5:def_1; then A14: ((f (#) f) || A) + ((f (#) g) || A) is integrable by A1, A2, A4, A5, A10, INTEGRA1:57; A15: ( (((f (#) f) || A) + ((f (#) g) || A)) | (A /\ A) is bounded & (((f (#) g) || A) + ((g (#) g) || A)) | (A /\ A) is bounded ) by A4, A5, A6, RFUNCT_1:83; |||((f + g),(f + g),A)||| = integral (((f (#) (f + g)) + (g (#) (f + g))) || A) by RFUNCT_1:10 .= integral (((f (#) (f + g)) || A) + ((g (#) (f + g)) || A)) by INTEGRA5:5 .= integral ((((f (#) f) + (f (#) g)) || A) + ((g (#) (f + g)) || A)) by RFUNCT_1:11 .= integral ((((f (#) f) + (f (#) g)) || A) + (((g (#) f) + (g (#) g)) || A)) by RFUNCT_1:11 .= integral ((((f (#) f) || A) + ((f (#) g) || A)) + (((g (#) f) + (g (#) g)) || A)) by INTEGRA5:5 .= integral ((((f (#) f) || A) + ((f (#) g) || A)) + (((g (#) f) || A) + ((g (#) g) || A))) by INTEGRA5:5 .= (integral (((f (#) f) || A) + ((f (#) g) || A))) + (integral (((f (#) g) || A) + ((g (#) g) || A))) by A1, A2, A3, A15, A14, A12, INTEGRA1:57 .= ((integral ((f (#) f) || A)) + (integral ((f (#) g) || A))) + (integral (((f (#) g) || A) + ((g (#) g) || A))) by A1, A2, A4, A5, A13, A10, INTEGRA1:57 .= ((integral ((f (#) f) || A)) + (integral ((f (#) g) || A))) + ((integral ((f (#) g) || A)) + (integral ((g (#) g) || A))) by A2, A3, A5, A6, A10, A11, INTEGRA1:57 ; hence |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| ; ::_thesis: verum end; begin definition let A be non empty closed_interval Subset of REAL; let f, g be PartFunc of REAL,REAL; predf is_orthogonal_with g,A means :Def2: :: INTEGRA9:def 2 |||(f,g,A)||| = 0 ; end; :: deftheorem Def2 defines is_orthogonal_with INTEGRA9:def_2_:_ for A being non empty closed_interval Subset of REAL for f, g being PartFunc of REAL,REAL holds ( f is_orthogonal_with g,A iff |||(f,g,A)||| = 0 ); theorem Th32: :: INTEGRA9:32 for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A holds |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| proof let f, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A holds |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A implies |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| ) assume ( (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A ) ; ::_thesis: ( not f is_orthogonal_with g,A or |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| ) then A1: |||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)||| by Th31; assume f is_orthogonal_with g,A ; ::_thesis: |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| then |||(f,g,A)||| = 0 by Def2; hence |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| by A1; ::_thesis: verum end; theorem :: INTEGRA9:33 for f being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & (f (#) f) || A is integrable & ( for x being Real st x in A holds ((f (#) f) || A) . x >= 0 ) holds |||(f,f,A)||| >= 0 by INTEGRA2:32; theorem :: INTEGRA9:34 for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds sin is_orthogonal_with cos ,A proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,PI.] implies sin is_orthogonal_with cos ,A ) assume A = [.0,PI.] ; ::_thesis: sin is_orthogonal_with cos ,A then |||(sin,cos,A)||| = 0 by INTEGRA8:92; hence sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum end; theorem :: INTEGRA9:35 for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds sin is_orthogonal_with cos ,A proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI * 2).] implies sin is_orthogonal_with cos ,A ) assume A = [.0,(PI * 2).] ; ::_thesis: sin is_orthogonal_with cos ,A then |||(sin,cos,A)||| = 0 by INTEGRA8:94; hence sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum end; theorem :: INTEGRA9:36 for n being Element of NAT for A being non empty closed_interval Subset of REAL st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds sin is_orthogonal_with cos ,A proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds sin is_orthogonal_with cos ,A let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] implies sin is_orthogonal_with cos ,A ) assume A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] ; ::_thesis: sin is_orthogonal_with cos ,A then |||(sin,cos,A)||| = 0 by INTEGRA8:95; hence sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum end; theorem :: INTEGRA9:37 for x being Real for n being Element of NAT for A being non empty closed_interval Subset of REAL st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds sin is_orthogonal_with cos ,A proof let x be Real; ::_thesis: for n being Element of NAT for A being non empty closed_interval Subset of REAL st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds sin is_orthogonal_with cos ,A let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds sin is_orthogonal_with cos ,A let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] implies sin is_orthogonal_with cos ,A ) assume A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] ; ::_thesis: sin is_orthogonal_with cos ,A then |||(sin,cos,A)||| = 0 by INTEGRA8:96; hence sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum end; theorem :: INTEGRA9:38 for A being non empty closed_interval Subset of REAL st A = [.(- PI),PI.] holds sin is_orthogonal_with cos ,A proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- PI),PI.] implies sin is_orthogonal_with cos ,A ) assume A = [.(- PI),PI.] ; ::_thesis: sin is_orthogonal_with cos ,A then A1: ( upper_bound A = PI & lower_bound A = - PI ) by INTEGRA8:37; |||(sin,cos,A)||| = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) by INTEGRA8:90 .= (1 / 2) * (((cos . PI) * (cos . (- PI))) - ((cos . PI) * (cos . PI))) by A1, SIN_COS:30 .= (1 / 2) * (((cos . PI) * (cos . PI)) - ((cos . PI) * (cos . PI))) by SIN_COS:30 ; hence sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum end; theorem :: INTEGRA9:39 for A being non empty closed_interval Subset of REAL st A = [.(- (PI / 2)),(PI / 2).] holds sin is_orthogonal_with cos ,A proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- (PI / 2)),(PI / 2).] implies sin is_orthogonal_with cos ,A ) assume A = [.(- (PI / 2)),(PI / 2).] ; ::_thesis: sin is_orthogonal_with cos ,A then A1: ( upper_bound A = PI / 2 & lower_bound A = - (PI / 2) ) by INTEGRA8:37; |||(sin,cos,A)||| = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) by INTEGRA8:90 .= (1 / 2) * (((cos . (PI / 2)) * (cos . (- (PI / 2)))) - ((cos . (PI / 2)) * (cos . (PI / 2)))) by A1, SIN_COS:30 .= (1 / 2) * (((cos . (PI / 2)) * (cos . (PI / 2))) - ((cos . (PI / 2)) * (cos . (PI / 2)))) by SIN_COS:30 ; hence sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum end; theorem :: INTEGRA9:40 for A being non empty closed_interval Subset of REAL st A = [.(- (2 * PI)),(2 * PI).] holds sin is_orthogonal_with cos ,A proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- (2 * PI)),(2 * PI).] implies sin is_orthogonal_with cos ,A ) assume A = [.(- (2 * PI)),(2 * PI).] ; ::_thesis: sin is_orthogonal_with cos ,A then A1: ( upper_bound A = 2 * PI & lower_bound A = - (2 * PI) ) by INTEGRA8:37; |||(sin,cos,A)||| = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) by INTEGRA8:90 .= (1 / 2) * (((cos . (2 * PI)) * (cos . (- (2 * PI)))) - ((cos . (2 * PI)) * (cos . (2 * PI)))) by A1, SIN_COS:30 .= (1 / 2) * (((cos . (2 * PI)) * (cos . (2 * PI))) - ((cos . (2 * PI)) * (cos . (2 * PI)))) by SIN_COS:30 ; hence sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum end; theorem :: INTEGRA9:41 for n being Element of NAT for A being non empty closed_interval Subset of REAL st A = [.(- ((2 * n) * PI)),((2 * n) * PI).] holds sin is_orthogonal_with cos ,A proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.(- ((2 * n) * PI)),((2 * n) * PI).] holds sin is_orthogonal_with cos ,A let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- ((2 * n) * PI)),((2 * n) * PI).] implies sin is_orthogonal_with cos ,A ) assume A = [.(- ((2 * n) * PI)),((2 * n) * PI).] ; ::_thesis: sin is_orthogonal_with cos ,A then A1: ( upper_bound A = (2 * n) * PI & lower_bound A = - ((2 * n) * PI) ) by INTEGRA8:37; |||(sin,cos,A)||| = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) by INTEGRA8:90 .= (1 / 2) * (((cos . ((2 * n) * PI)) * (cos . (- ((2 * n) * PI)))) - ((cos . ((2 * n) * PI)) * (cos . ((2 * n) * PI)))) by A1, SIN_COS:30 .= (1 / 2) * (((cos . ((2 * n) * PI)) * (cos . ((2 * n) * PI))) - ((cos . ((2 * n) * PI)) * (cos . ((2 * n) * PI)))) by SIN_COS:30 ; hence sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum end; theorem :: INTEGRA9:42 for x being Real for n being Element of NAT for A being non empty closed_interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds sin is_orthogonal_with cos ,A proof let x be Real; ::_thesis: for n being Element of NAT for A being non empty closed_interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds sin is_orthogonal_with cos ,A let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] holds sin is_orthogonal_with cos ,A let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] implies sin is_orthogonal_with cos ,A ) assume A = [.(x - ((2 * n) * PI)),(x + ((2 * n) * PI)).] ; ::_thesis: sin is_orthogonal_with cos ,A then A1: ( upper_bound A = x + ((2 * n) * PI) & lower_bound A = x - ((2 * n) * PI) ) by INTEGRA8:37; |||(sin,cos,A)||| = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) by INTEGRA8:90 .= (1 / 2) * (((cos . (((2 * n) * PI) - x)) * (cos . (- (((2 * n) * PI) - x)))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by A1, SIN_COS:30 .= (1 / 2) * (((cos . ((- x) + ((2 * n) * PI))) * (cos . ((- x) + ((2 * n) * PI)))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by SIN_COS:30 .= (1 / 2) * (((cos (- x)) * (cos ((- x) + ((2 * n) * PI)))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by INTEGRA8:3 .= (1 / 2) * (((cos (- x)) * (cos (- x))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by INTEGRA8:3 .= (1 / 2) * (((cos x) * (cos (- x))) - ((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by SIN_COS:31 .= (1 / 2) * (((cos x) * (cos x)) - ((cos (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))))) by SIN_COS:31 .= (1 / 2) * (((cos x) * (cos x)) - ((cos x) * (cos (x + ((2 * n) * PI))))) by INTEGRA8:3 .= (1 / 2) * (((cos x) * (cos x)) - ((cos x) * (cos x))) by INTEGRA8:3 ; hence sin is_orthogonal_with cos ,A by Def2; ::_thesis: verum end; begin definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,REAL; func||..f,A..|| -> Real equals :: INTEGRA9:def 3 sqrt |||(f,f,A)|||; correctness coherence sqrt |||(f,f,A)||| is Real; ; end; :: deftheorem defines ||.. INTEGRA9:def_3_:_ for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL holds ||..f,A..|| = sqrt |||(f,f,A)|||; theorem :: INTEGRA9:43 for f being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds ((f (#) f) || A) . x >= 0 ) holds 0 <= ||..f,A..|| proof let f be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds ((f (#) f) || A) . x >= 0 ) holds 0 <= ||..f,A..|| let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) f) || A is total & ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds ((f (#) f) || A) . x >= 0 ) implies 0 <= ||..f,A..|| ) assume A1: (f (#) f) || A is total ; ::_thesis: ( not ((f (#) f) || A) | A is bounded or ex x being Real st ( x in A & not ((f (#) f) || A) . x >= 0 ) or 0 <= ||..f,A..|| ) assume ( ((f (#) f) || A) | A is bounded & ( for x being Real st x in A holds ((f (#) f) || A) . x >= 0 ) ) ; ::_thesis: 0 <= ||..f,A..|| then |||(f,f,A)||| >= 0 by A1, INTEGRA2:32; hence 0 <= ||..f,A..|| by SQUARE_1:def_2; ::_thesis: verum end; theorem :: INTEGRA9:44 for f being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL holds ||..(1 (#) f),A..|| = ||..f,A..|| by RFUNCT_1:21; theorem :: INTEGRA9:45 for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A & ( for x being Real st x in A holds ((f (#) f) || A) . x >= 0 ) & ( for x being Real st x in A holds ((g (#) g) || A) . x >= 0 ) holds ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A & ( for x being Real st x in A holds ((f (#) f) || A) . x >= 0 ) & ( for x being Real st x in A holds ((g (#) g) || A) . x >= 0 ) holds ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) let A be non empty closed_interval Subset of REAL; ::_thesis: ( (f (#) f) || A is total & (f (#) g) || A is total & (g (#) g) || A is total & ((f (#) f) || A) | A is bounded & ((f (#) g) || A) | A is bounded & ((g (#) g) || A) | A is bounded & f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A & f is_orthogonal_with g,A & ( for x being Real st x in A holds ((f (#) f) || A) . x >= 0 ) & ( for x being Real st x in A holds ((g (#) g) || A) . x >= 0 ) implies ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) ) assume that A1: (f (#) f) || A is total and A2: (f (#) g) || A is total and A3: (g (#) g) || A is total and A4: ((f (#) f) || A) | A is bounded and A5: ((f (#) g) || A) | A is bounded and A6: ((g (#) g) || A) | A is bounded and A7: ( f (#) f is_integrable_on A & f (#) g is_integrable_on A & g (#) g is_integrable_on A ) ; ::_thesis: ( not f is_orthogonal_with g,A or ex x being Real st ( x in A & not ((f (#) f) || A) . x >= 0 ) or ex x being Real st ( x in A & not ((g (#) g) || A) . x >= 0 ) or ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) ) assume A8: f is_orthogonal_with g,A ; ::_thesis: ( ex x being Real st ( x in A & not ((f (#) f) || A) . x >= 0 ) or ex x being Real st ( x in A & not ((g (#) g) || A) . x >= 0 ) or ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) ) assume for x being Real st x in A holds ((f (#) f) || A) . x >= 0 ; ::_thesis: ( ex x being Real st ( x in A & not ((g (#) g) || A) . x >= 0 ) or ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) ) then A9: |||(f,f,A)||| >= 0 by A1, A4, INTEGRA2:32; assume for x being Real st x in A holds ((g (#) g) || A) . x >= 0 ; ::_thesis: ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) then A10: |||(g,g,A)||| >= 0 by A3, A6, INTEGRA2:32; then A11: ||..g,A..|| ^2 = |||(g,g,A)||| by SQUARE_1:def_2; |||((f + g),(f + g),A)||| = |||(f,f,A)||| + |||(g,g,A)||| by A1, A2, A3, A4, A5, A6, A7, A8, Th32; then |||((f + g),(f + g),A)||| >= 0 by A9, A10, XREAL_1:33; then A12: ||..(f + g),A..|| ^2 = |||((f + g),(f + g),A)||| by SQUARE_1:def_2; ||..f,A..|| ^2 = |||(f,f,A)||| by A9, SQUARE_1:def_2; hence ||..(f + g),A..|| ^2 = (||..f,A..|| ^2) + (||..g,A..|| ^2) by A1, A2, A3, A4, A5, A6, A7, A8, A12, A11, Th32; ::_thesis: verum end; begin theorem :: INTEGRA9:46 for a being Real for A being non empty closed_interval Subset of REAL st not - a in A holds ((AffineMap (1,a)) ^) | A is continuous proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL st not - a in A holds ((AffineMap (1,a)) ^) | A is continuous let A be non empty closed_interval Subset of REAL; ::_thesis: ( not - a in A implies ((AffineMap (1,a)) ^) | A is continuous ) set g2 = AffineMap (1,a); assume A1: not - a in A ; ::_thesis: ((AffineMap (1,a)) ^) | A is continuous not 0 in rng ((AffineMap (1,a)) | A) proof set h2 = (AffineMap (1,a)) | A; assume 0 in rng ((AffineMap (1,a)) | A) ; ::_thesis: contradiction then consider x being set such that A2: x in dom ((AffineMap (1,a)) | A) and A3: ((AffineMap (1,a)) | A) . x = 0 by FUNCT_1:def_3; reconsider d = x as Real by A2; A4: (AffineMap (1,a)) . d = a + (1 * d) by FCONT_1:def_4; d in A by A2, RELAT_1:57; then ( dom ((AffineMap (1,a)) | A) c= A & a + d = 0 ) by A3, A4, FUNCT_1:49, RELAT_1:58; hence contradiction by A1, A2; ::_thesis: verum end; then A5: ((AffineMap (1,a)) | A) " {0} = {} by FUNCT_1:72; thus ((AffineMap (1,a)) ^) | A is continuous by A5, FCONT_1:23; ::_thesis: verum end; theorem :: INTEGRA9:47 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) let f, f2 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 = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous holds integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (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 = a + x & f . x <> 0 ) ) & Z = dom f & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = - (1 / ((a + x) ^2)) ) & f2 | A is continuous implies integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) and A3: Z = dom f and A4: dom f = dom f2 and A5: for x being Real st x in Z holds f2 . x = - (1 / ((a + x) ^2)) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: f ^ is_differentiable_on Z by A2, A3, FDIFF_4:14; A9: for x being Real st x in dom ((f ^) `| Z) holds ((f ^) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom ((f ^) `| Z) implies ((f ^) `| Z) . x = f2 . x ) assume x in dom ((f ^) `| Z) ; ::_thesis: ((f ^) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) by A2, A3, FDIFF_4:14 .= f2 . x by A5, A10 ; hence ((f ^) `| Z) . x = f2 . x ; ::_thesis: verum end; dom ((f ^) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then (f ^) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:48 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A)) let f, f2 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 = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous holds integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (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 = a + x & f . x <> 0 ) ) & dom ((- 1) (#) (f ^)) = Z & dom ((- 1) (#) (f ^)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a + x) ^2) ) & f2 | A is continuous implies integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) and A3: dom ((- 1) (#) (f ^)) = Z and A4: dom ((- 1) (#) (f ^)) = dom f2 and A5: for x being Real st x in Z holds f2 . x = 1 / ((a + x) ^2) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: (- 1) (#) (f ^) is_differentiable_on Z by A2, A3, FDIFF_4:15; A9: for x being Real st x in dom (((- 1) (#) (f ^)) `| Z) holds (((- 1) (#) (f ^)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((- 1) (#) (f ^)) `| Z) implies (((- 1) (#) (f ^)) `| Z) . x = f2 . x ) assume x in dom (((- 1) (#) (f ^)) `| Z) ; ::_thesis: (((- 1) (#) (f ^)) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) by A2, A3, FDIFF_4:15 .= f2 . x by A5, A10 ; hence (((- 1) (#) (f ^)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((- 1) (#) (f ^)) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then ((- 1) (#) (f ^)) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = (((- 1) (#) (f ^)) . (upper_bound A)) - (((- 1) (#) (f ^)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:49 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) let f, f2 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 = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous holds integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (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 = a - x & f . x <> 0 ) ) & dom f = Z & dom f = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / ((a - x) ^2) ) & f2 | A is continuous implies integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = a - x & f . x <> 0 ) and A3: dom f = Z and A4: dom f = dom f2 and A5: for x being Real st x in Z holds f2 . x = 1 / ((a - x) ^2) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: f ^ is_differentiable_on Z by A2, A3, FDIFF_4:16; A9: for x being Real st x in dom ((f ^) `| Z) holds ((f ^) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom ((f ^) `| Z) implies ((f ^) `| Z) . x = f2 . x ) assume x in dom ((f ^) `| Z) ; ::_thesis: ((f ^) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then ((f ^) `| Z) . x = 1 / ((a - x) ^2) by A2, A3, FDIFF_4:16 .= f2 . x by A5, A10 ; hence ((f ^) `| Z) . x = f2 . x ; ::_thesis: verum end; dom ((f ^) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then (f ^) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = ((f ^) . (upper_bound A)) - ((f ^) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:50 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a + x) ) & f2 | A is continuous holds integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a + x) ) & f2 | A is continuous holds integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a + x) ) & f2 | A is continuous holds integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) let f, f2 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 = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a + x) ) & f2 | A is continuous holds integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (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 = a + x & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a + x) ) & f2 | A is continuous implies integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) and A3: dom (ln * f) = Z and A4: dom (ln * f) = dom f2 and A5: for x being Real st x in Z holds f2 . x = 1 / (a + x) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: ln * f is_differentiable_on Z by A2, A3, FDIFF_4:1; A9: for x being Real st x in dom ((ln * f) `| Z) holds ((ln * f) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom ((ln * f) `| Z) implies ((ln * f) `| Z) . x = f2 . x ) assume x in dom ((ln * f) `| Z) ; ::_thesis: ((ln * f) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then ((ln * f) `| Z) . x = 1 / (a + x) by A2, A3, FDIFF_4:1 .= f2 . x by A5, A10 ; hence ((ln * f) `| Z) . x = f2 . x ; ::_thesis: verum end; dom ((ln * f) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then (ln * f) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:51 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (x - a) ) & f2 | A is continuous holds integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (x - a) ) & f2 | A is continuous holds integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (x - a) ) & f2 | A is continuous holds integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) let f, f2 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 = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (x - a) ) & f2 | A is continuous holds integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (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 = x - a & f . x > 0 ) ) & dom (ln * f) = Z & dom (ln * f) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (x - a) ) & f2 | A is continuous implies integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = x - a & f . x > 0 ) and A3: dom (ln * f) = Z and A4: dom (ln * f) = dom f2 and A5: for x being Real st x in Z holds f2 . x = 1 / (x - a) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: ln * f is_differentiable_on Z by A2, A3, FDIFF_4:2; A9: for x being Real st x in dom ((ln * f) `| Z) holds ((ln * f) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom ((ln * f) `| Z) implies ((ln * f) `| Z) . x = f2 . x ) assume x in dom ((ln * f) `| Z) ; ::_thesis: ((ln * f) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then ((ln * f) `| Z) . x = 1 / (x - a) by A2, A3, FDIFF_4:2 .= f2 . x by A5, A10 ; hence ((ln * f) `| Z) . x = f2 . x ; ::_thesis: verum end; dom ((ln * f) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then (ln * f) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = ((ln * f) . (upper_bound A)) - ((ln * f) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:52 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a - x) ) & f2 | A is continuous holds integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a - x) ) & f2 | A is continuous holds integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a - x) ) & f2 | A is continuous holds integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A)) let f, f2 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 = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a - x) ) & f2 | A is continuous holds integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (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 = a - x & f . x > 0 ) ) & dom (- (ln * f)) = Z & dom (- (ln * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = 1 / (a - x) ) & f2 | A is continuous implies integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) and A3: dom (- (ln * f)) = Z and A4: dom (- (ln * f)) = dom f2 and A5: for x being Real st x in Z holds f2 . x = 1 / (a - x) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: - (ln * f) is_differentiable_on Z by A2, A3, FDIFF_4:3; A9: for x being Real st x in dom ((- (ln * f)) `| Z) holds ((- (ln * f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom ((- (ln * f)) `| Z) implies ((- (ln * f)) `| Z) . x = f2 . x ) assume x in dom ((- (ln * f)) `| Z) ; ::_thesis: ((- (ln * f)) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then ((- (ln * f)) `| Z) . x = 1 / (a - x) by A2, A3, FDIFF_4:3 .= f2 . x by A5, A10 ; hence ((- (ln * f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom ((- (ln * f)) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then (- (ln * f)) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = ((- (ln * f)) . (upper_bound A)) - ((- (ln * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:53 for a being Real for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = x / (a + x) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = x / (a + x) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = x / (a + x) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A)) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = x / (a + x) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = x / (a + x) ) & f2 | A is continuous implies integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: ( f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom ((id Z) - (a (#) f)) = Z ) and A3: Z = dom f2 and A4: for x being Real st x in Z holds f2 . x = x / (a + x) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A)) A6: f2 is_integrable_on A by A1, A3, A5, INTEGRA5:11; A7: (id Z) - (a (#) f) is_differentiable_on Z by A2, FDIFF_4:4; A8: for x being Real st x in dom (((id Z) - (a (#) f)) `| Z) holds (((id Z) - (a (#) f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((id Z) - (a (#) f)) `| Z) implies (((id Z) - (a (#) f)) `| Z) . x = f2 . x ) assume x in dom (((id Z) - (a (#) f)) `| Z) ; ::_thesis: (((id Z) - (a (#) f)) `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) by A2, FDIFF_4:4 .= f2 . x by A4, A9 ; hence (((id Z) - (a (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((id Z) - (a (#) f)) `| Z) = dom f2 by A3, A7, FDIFF_1:def_7; then ((id Z) - (a (#) f)) `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = (((id Z) - (a (#) f)) . (upper_bound A)) - (((id Z) - (a (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:54 for a being Real for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) / (a + x) ) & f2 | A is continuous holds integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) / (a + x) ) & f2 | A is continuous holds integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) / (a + x) ) & f2 | A is continuous holds integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A)) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) / (a + x) ) & f2 | A is continuous holds integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) / (a + x) ) & f2 | A is continuous implies integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A)) ) assume that A1: A c= Z and A2: ( f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) & dom (((2 * a) (#) f) - (id Z)) = Z ) and A3: Z = dom f2 and A4: for x being Real st x in Z holds f2 . x = (a - x) / (a + x) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A)) A6: f2 is_integrable_on A by A1, A3, A5, INTEGRA5:11; A7: ((2 * a) (#) f) - (id Z) is_differentiable_on Z by A2, FDIFF_4:5; A8: for x being Real st x in dom ((((2 * a) (#) f) - (id Z)) `| Z) holds ((((2 * a) (#) f) - (id Z)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom ((((2 * a) (#) f) - (id Z)) `| Z) implies ((((2 * a) (#) f) - (id Z)) `| Z) . x = f2 . x ) assume x in dom ((((2 * a) (#) f) - (id Z)) `| Z) ; ::_thesis: ((((2 * a) (#) f) - (id Z)) `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) by A2, FDIFF_4:5 .= f2 . x by A4, A9 ; hence ((((2 * a) (#) f) - (id Z)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom ((((2 * a) (#) f) - (id Z)) `| Z) = dom f2 by A3, A7, FDIFF_1:def_7; then (((2 * a) (#) f) - (id Z)) `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = ((((2 * a) (#) f) - (id Z)) . (upper_bound A)) - ((((2 * a) (#) f) - (id Z)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:55 for a being Real for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + a) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + a) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + a) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A)) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + a) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + a) ) & f2 | A is continuous implies integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: ( f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) & dom ((id Z) - ((2 * a) (#) f)) = Z ) and A3: Z = dom f2 and A4: for x being Real st x in Z holds f2 . x = (x - a) / (x + a) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A)) A6: f2 is_integrable_on A by A1, A3, A5, INTEGRA5:11; A7: (id Z) - ((2 * a) (#) f) is_differentiable_on Z by A2, FDIFF_4:6; A8: for x being Real st x in dom (((id Z) - ((2 * a) (#) f)) `| Z) holds (((id Z) - ((2 * a) (#) f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((id Z) - ((2 * a) (#) f)) `| Z) implies (((id Z) - ((2 * a) (#) f)) `| Z) . x = f2 . x ) assume x in dom (((id Z) - ((2 * a) (#) f)) `| Z) ; ::_thesis: (((id Z) - ((2 * a) (#) f)) `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) by A2, FDIFF_4:6 .= f2 . x by A4, A9 ; hence (((id Z) - ((2 * a) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((id Z) - ((2 * a) (#) f)) `| Z) = dom f2 by A3, A7, FDIFF_1:def_7; then ((id Z) - ((2 * a) (#) f)) `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = (((id Z) - ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) - ((2 * a) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:56 for a being Real for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - a) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - a) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - a) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A)) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - a) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - a) ) & f2 | A is continuous implies integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: ( f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) & dom ((id Z) + ((2 * a) (#) f)) = Z ) and A3: Z = dom f2 and A4: for x being Real st x in Z holds f2 . x = (x + a) / (x - a) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A)) A6: f2 is_integrable_on A by A1, A3, A5, INTEGRA5:11; A7: (id Z) + ((2 * a) (#) f) is_differentiable_on Z by A2, FDIFF_4:7; A8: for x being Real st x in dom (((id Z) + ((2 * a) (#) f)) `| Z) holds (((id Z) + ((2 * a) (#) f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((id Z) + ((2 * a) (#) f)) `| Z) implies (((id Z) + ((2 * a) (#) f)) `| Z) . x = f2 . x ) assume x in dom (((id Z) + ((2 * a) (#) f)) `| Z) ; ::_thesis: (((id Z) + ((2 * a) (#) f)) `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) by A2, FDIFF_4:7 .= f2 . x by A4, A9 ; hence (((id Z) + ((2 * a) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((id Z) + ((2 * a) (#) f)) `| Z) = dom f2 by A3, A7, FDIFF_1:def_7; then ((id Z) + ((2 * a) (#) f)) `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = (((id Z) + ((2 * a) (#) f)) . (upper_bound A)) - (((id Z) + ((2 * a) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:57 for b, a being Real for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x + b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A)) proof let b, a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x + b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x + b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A)) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x + b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x + b) ) & f2 | A is continuous implies integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: ( f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) + ((a - b) (#) f)) = Z ) and A3: Z = dom f2 and A4: for x being Real st x in Z holds f2 . x = (x + a) / (x + b) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A)) A6: f2 is_integrable_on A by A1, A3, A5, INTEGRA5:11; A7: (id Z) + ((a - b) (#) f) is_differentiable_on Z by A2, FDIFF_4:8; A8: for x being Real st x in dom (((id Z) + ((a - b) (#) f)) `| Z) holds (((id Z) + ((a - b) (#) f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((id Z) + ((a - b) (#) f)) `| Z) implies (((id Z) + ((a - b) (#) f)) `| Z) . x = f2 . x ) assume x in dom (((id Z) + ((a - b) (#) f)) `| Z) ; ::_thesis: (((id Z) + ((a - b) (#) f)) `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) by A2, FDIFF_4:8 .= f2 . x by A4, A9 ; hence (((id Z) + ((a - b) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((id Z) + ((a - b) (#) f)) `| Z) = dom f2 by A3, A7, FDIFF_1:def_7; then ((id Z) + ((a - b) (#) f)) `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = (((id Z) + ((a - b) (#) f)) . (upper_bound A)) - (((id Z) + ((a - b) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:58 for b, a being Real for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A)) proof let b, a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A)) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x + a) / (x - b) ) & f2 | A is continuous implies integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: ( f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((a + b) (#) f)) = Z ) and A3: Z = dom f2 and A4: for x being Real st x in Z holds f2 . x = (x + a) / (x - b) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A)) A6: f2 is_integrable_on A by A1, A3, A5, INTEGRA5:11; A7: (id Z) + ((a + b) (#) f) is_differentiable_on Z by A2, FDIFF_4:9; A8: for x being Real st x in dom (((id Z) + ((a + b) (#) f)) `| Z) holds (((id Z) + ((a + b) (#) f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((id Z) + ((a + b) (#) f)) `| Z) implies (((id Z) + ((a + b) (#) f)) `| Z) . x = f2 . x ) assume x in dom (((id Z) + ((a + b) (#) f)) `| Z) ; ::_thesis: (((id Z) + ((a + b) (#) f)) `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) by A2, FDIFF_4:9 .= f2 . x by A4, A9 ; hence (((id Z) + ((a + b) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((id Z) + ((a + b) (#) f)) `| Z) = dom f2 by A3, A7, FDIFF_1:def_7; then ((id Z) + ((a + b) (#) f)) `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = (((id Z) + ((a + b) (#) f)) . (upper_bound A)) - (((id Z) + ((a + b) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:59 for b, a being Real for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A)) proof let b, a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A)) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x + b) ) & f2 | A is continuous implies integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: ( f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) & dom ((id Z) - ((a + b) (#) f)) = Z ) and A3: Z = dom f2 and A4: for x being Real st x in Z holds f2 . x = (x - a) / (x + b) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A)) A6: f2 is_integrable_on A by A1, A3, A5, INTEGRA5:11; A7: (id Z) - ((a + b) (#) f) is_differentiable_on Z by A2, FDIFF_4:10; A8: for x being Real st x in dom (((id Z) - ((a + b) (#) f)) `| Z) holds (((id Z) - ((a + b) (#) f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((id Z) - ((a + b) (#) f)) `| Z) implies (((id Z) - ((a + b) (#) f)) `| Z) . x = f2 . x ) assume x in dom (((id Z) - ((a + b) (#) f)) `| Z) ; ::_thesis: (((id Z) - ((a + b) (#) f)) `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) by A2, FDIFF_4:10 .= f2 . x by A4, A9 ; hence (((id Z) - ((a + b) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((id Z) - ((a + b) (#) f)) `| Z) = dom f2 by A3, A7, FDIFF_1:def_7; then ((id Z) - ((a + b) (#) f)) `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = (((id Z) - ((a + b) (#) f)) . (upper_bound A)) - (((id Z) - ((a + b) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:60 for b, a being Real for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x - b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A)) proof let b, a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x - b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x - b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A)) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x - b) ) & f2 | A is continuous holds integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z & Z = dom f2 & ( for x being Real st x in Z holds f2 . x = (x - a) / (x - b) ) & f2 | A is continuous implies integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: ( f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) & dom ((id Z) + ((b - a) (#) f)) = Z ) and A3: Z = dom f2 and A4: for x being Real st x in Z holds f2 . x = (x - a) / (x - b) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A)) A6: f2 is_integrable_on A by A1, A3, A5, INTEGRA5:11; A7: (id Z) + ((b - a) (#) f) is_differentiable_on Z by A2, FDIFF_4:11; A8: for x being Real st x in dom (((id Z) + ((b - a) (#) f)) `| Z) holds (((id Z) + ((b - a) (#) f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((id Z) + ((b - a) (#) f)) `| Z) implies (((id Z) + ((b - a) (#) f)) `| Z) . x = f2 . x ) assume x in dom (((id Z) + ((b - a) (#) f)) `| Z) ; ::_thesis: (((id Z) + ((b - a) (#) f)) `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) by A2, FDIFF_4:11 .= f2 . x by A4, A9 ; hence (((id Z) + ((b - a) (#) f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((id Z) + ((b - a) (#) f)) `| Z) = dom f2 by A3, A7, FDIFF_1:def_7; then ((id Z) + ((b - a) (#) f)) `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = (((id Z) + ((b - a) (#) f)) . (upper_bound A)) - (((id Z) + ((b - a) (#) f)) . (lower_bound A)) by A1, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:61 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & dom ln = Z & Z = dom ((id Z) ^) & ((id Z) ^) | A is continuous holds integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (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 & dom ln = Z & Z = dom ((id Z) ^) & ((id Z) ^) | A is continuous holds integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & dom ln = Z & Z = dom ((id Z) ^) & ((id Z) ^) | A is continuous implies integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A)) ) set f2 = (id Z) ^ ; assume that A1: A c= Z and A2: dom ln = Z and A3: Z = dom ((id Z) ^) and A4: ((id Z) ^) | A is continuous ; ::_thesis: integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A)) A5: (id Z) ^ is_integrable_on A by A1, A3, A4, INTEGRA5:11; A6: ln is_differentiable_on Z by A2, FDIFF_5:19; A7: for x being Real st x in dom (ln `| Z) holds (ln `| Z) . x = ((id Z) ^) . x proof let x be Real; ::_thesis: ( x in dom (ln `| Z) implies (ln `| Z) . x = ((id Z) ^) . x ) assume x in dom (ln `| Z) ; ::_thesis: (ln `| Z) . x = ((id Z) ^) . x then A8: x in Z by A6, FDIFF_1:def_7; then (ln `| Z) . x = 1 / x by A2, FDIFF_5:19 .= x " by XCMPLX_1:215 .= ((id Z) . x) " by A8, FUNCT_1:18 .= ((id Z) ^) . x by A3, A8, RFUNCT_1:def_2 ; hence (ln `| Z) . x = ((id Z) ^) . x ; ::_thesis: verum end; dom (ln `| Z) = dom ((id Z) ^) by A3, A6, FDIFF_1:def_7; then ln `| Z = (id Z) ^ by A7, PARTFUN1:5; hence integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A)) by A1, A3, A4, A5, A6, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:62 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f2 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 x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds f2 . x = n / x ) & f2 | A is continuous holds integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A)) proof let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f2 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 x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds f2 . x = n / x ) & f2 | A is continuous holds integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f2 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 x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds f2 . x = n / x ) & f2 | A is continuous holds integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A)) let f2 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 x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds f2 . x = n / x ) & f2 | A is continuous holds integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & ( for x being Real st x in Z holds x > 0 ) & dom (ln * (#Z n)) = Z & dom (ln * (#Z n)) = dom f2 & ( for x being Real st x in Z holds f2 . x = n / x ) & f2 | A is continuous implies integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds x > 0 and A3: dom (ln * (#Z n)) = Z and A4: dom (ln * (#Z n)) = dom f2 and A5: for x being Real st x in Z holds f2 . x = n / x and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: ln * (#Z n) is_differentiable_on Z by A2, A3, FDIFF_6:9; A9: for x being Real st x in dom ((ln * (#Z n)) `| Z) holds ((ln * (#Z n)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom ((ln * (#Z n)) `| Z) implies ((ln * (#Z n)) `| Z) . x = f2 . x ) assume x in dom ((ln * (#Z n)) `| Z) ; ::_thesis: ((ln * (#Z n)) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then ((ln * (#Z n)) `| Z) . x = n / x by A2, A3, FDIFF_6:9 .= f2 . x by A5, A10 ; hence ((ln * (#Z n)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom ((ln * (#Z n)) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then (ln * (#Z n)) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = ((ln * (#Z n)) . (upper_bound A)) - ((ln * (#Z n)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:63 for A being non empty closed_interval Subset of REAL for f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real st x in Z holds f2 . x = - (1 / x) ) & f2 | A is continuous holds integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f2 being PartFunc of REAL,REAL for Z being open Subset of REAL st not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real st x in Z holds f2 . x = - (1 / x) ) & f2 | A is continuous holds integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A)) let f2 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real st x in Z holds f2 . x = - (1 / x) ) & f2 | A is continuous holds integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & A c= Z & dom (ln * ((id Z) ^)) = Z & dom (ln * ((id Z) ^)) = dom f2 & ( for x being Real st x in Z holds f2 . x = - (1 / x) ) & f2 | A is continuous implies integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A)) ) set f = id Z; assume that A1: not 0 in Z and A2: A c= Z and A3: dom (ln * ((id Z) ^)) = Z and A4: dom (ln * ((id Z) ^)) = dom f2 and A5: for x being Real st x in Z holds f2 . x = - (1 / x) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A)) A7: f2 is_integrable_on A by A2, A3, A4, A6, INTEGRA5:11; A8: ln * ((id Z) ^) is_differentiable_on Z by A1, A3, FDIFF_8:5; A9: for x being Real st x in dom ((ln * ((id Z) ^)) `| Z) holds ((ln * ((id Z) ^)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom ((ln * ((id Z) ^)) `| Z) implies ((ln * ((id Z) ^)) `| Z) . x = f2 . x ) assume x in dom ((ln * ((id Z) ^)) `| Z) ; ::_thesis: ((ln * ((id Z) ^)) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then ((ln * ((id Z) ^)) `| Z) . x = - (1 / x) by A1, A3, FDIFF_8:5 .= f2 . x by A5, A10 ; hence ((ln * ((id Z) ^)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom ((ln * ((id Z) ^)) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then (ln * ((id Z) ^)) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = ((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A)) by A2, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:64 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) let f, f2 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 = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous holds integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (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 = a + x & f . x > 0 ) ) & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z & dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (1 / 2) ) & f2 | A is continuous implies integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) and A3: dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = Z and A4: dom ((2 / 3) (#) ((#R (3 / 2)) * f)) = dom f2 and A5: for x being Real st x in Z holds f2 . x = (a + x) #R (1 / 2) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z by A2, A3, FDIFF_4:28; A9: for x being Real st x in dom (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) holds (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) implies (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x ) assume x in dom (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) ; ::_thesis: (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) by A2, A3, FDIFF_4:28 .= f2 . x by A5, A10 ; hence (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then ((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = (((2 / 3) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((2 / 3) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:65 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) let f, f2 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 = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous holds integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (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 = a - x & f . x > 0 ) ) & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z & dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (1 / 2) ) & f2 | A is continuous implies integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) and A3: dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = Z and A4: dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) = dom f2 and A5: for x being Real st x in Z holds f2 . x = (a - x) #R (1 / 2) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z by A2, A3, FDIFF_4:29; A9: for x being Real st x in dom (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) holds (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) implies (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x ) assume x in dom (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) ; ::_thesis: (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) by A2, A3, FDIFF_4:29 .= f2 . x by A5, A10 ; hence (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (upper_bound A)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:66 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A)) let f, f2 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 = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous holds integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (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 = a + x & f . x > 0 ) ) & dom (2 (#) ((#R (1 / 2)) * f)) = Z & dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a + x) #R (- (1 / 2)) ) & f2 | A is continuous implies integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) and A3: dom (2 (#) ((#R (1 / 2)) * f)) = Z and A4: dom (2 (#) ((#R (1 / 2)) * f)) = dom f2 and A5: for x being Real st x in Z holds f2 . x = (a + x) #R (- (1 / 2)) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z by A2, A3, FDIFF_4:30; A9: for x being Real st x in dom ((2 (#) ((#R (1 / 2)) * f)) `| Z) holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom ((2 (#) ((#R (1 / 2)) * f)) `| Z) implies ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x ) assume x in dom ((2 (#) ((#R (1 / 2)) * f)) `| Z) ; ::_thesis: ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) by A2, A3, FDIFF_4:30 .= f2 . x by A5, A10 ; hence ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom ((2 (#) ((#R (1 / 2)) * f)) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then (2 (#) ((#R (1 / 2)) * f)) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = ((2 (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - ((2 (#) ((#R (1 / 2)) * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:67 for a being Real for A being non empty closed_interval Subset of REAL for f, f2 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 = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A)) proof let a be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f, f2 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 = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f, f2 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 = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A)) let f, f2 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 = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous holds integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (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 = a - x & f . x > 0 ) ) & dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z & dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 & ( for x being Real st x in Z holds f2 . x = (a - x) #R (- (1 / 2)) ) & f2 | A is continuous implies integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A)) ) assume that A1: A c= Z and A2: for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) and A3: dom ((- 2) (#) ((#R (1 / 2)) * f)) = Z and A4: dom ((- 2) (#) ((#R (1 / 2)) * f)) = dom f2 and A5: for x being Real st x in Z holds f2 . x = (a - x) #R (- (1 / 2)) and A6: f2 | A is continuous ; ::_thesis: integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A)) A7: f2 is_integrable_on A by A1, A3, A4, A6, INTEGRA5:11; A8: (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z by A2, A3, FDIFF_4:31; A9: for x being Real st x in dom (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) holds (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) implies (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x ) assume x in dom (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) ; ::_thesis: (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x then A10: x in Z by A8, FDIFF_1:def_7; then (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) by A2, A3, FDIFF_4:31 .= f2 . x by A5, A10 ; hence (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = f2 . x ; ::_thesis: verum end; dom (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) = dom f2 by A3, A4, A8, FDIFF_1:def_7; then ((- 2) (#) ((#R (1 / 2)) * f)) `| Z = f2 by A9, PARTFUN1:5; hence integral (f2,A) = (((- 2) (#) ((#R (1 / 2)) * f)) . (upper_bound A)) - (((- 2) (#) ((#R (1 / 2)) * f)) . (lower_bound A)) by A1, A3, A4, A6, A7, A8, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:68 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 & dom (((- (id Z)) (#) cos) + sin) = Z & ( for x being Real st x in Z holds f . x = x * (sin . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) 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 & dom (((- (id Z)) (#) cos) + sin) = Z & ( for x being Real st x in Z holds f . x = x * (sin . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & dom (((- (id Z)) (#) cos) + sin) = Z & ( for x being Real st x in Z holds f . x = x * (sin . x) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & dom (((- (id Z)) (#) cos) + sin) = Z & ( for x being Real st x in Z holds f . x = x * (sin . x) ) & Z = dom f & f | A is continuous implies integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) ) assume that A1: A c= Z and A2: dom (((- (id Z)) (#) cos) + sin) = Z and A3: for x being Real st x in Z holds f . x = x * (sin . x) and A4: Z = dom f and A5: f | A is continuous ; ::_thesis: integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) A6: ((- (id Z)) (#) cos) + sin is_differentiable_on Z by A2, FDIFF_4:46; A7: for x being Real st x in dom ((((- (id Z)) (#) cos) + sin) `| Z) holds ((((- (id Z)) (#) cos) + sin) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((((- (id Z)) (#) cos) + sin) `| Z) implies ((((- (id Z)) (#) cos) + sin) `| Z) . x = f . x ) assume x in dom ((((- (id Z)) (#) cos) + sin) `| Z) ; ::_thesis: ((((- (id Z)) (#) cos) + sin) `| Z) . x = f . x then A8: x in Z by A6, FDIFF_1:def_7; then ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) by A2, FDIFF_4:46 .= f . x by A3, A8 ; hence ((((- (id Z)) (#) cos) + sin) `| Z) . x = f . x ; ::_thesis: verum end; dom ((((- (id Z)) (#) cos) + sin) `| Z) = dom f by A4, A6, FDIFF_1:def_7; then A9: (((- (id Z)) (#) cos) + sin) `| Z = f by A7, PARTFUN1:5; ( f is_integrable_on A & f | A is bounded ) by A1, A4, A5, INTEGRA5:10, INTEGRA5:11; hence integral (f,A) = ((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) by A1, A2, A9, FDIFF_4:46, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA9:69 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 & dom sec = Z & ( for x being Real st x in Z holds f . x = (sin . x) / ((cos . x) ^2) ) & Z = dom f & f | A is continuous holds integral (f,A) = (sec . (upper_bound A)) - (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 & dom sec = Z & ( for x being Real st x in Z holds f . x = (sin . x) / ((cos . x) ^2) ) & Z = dom f & f | A is continuous holds integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & dom sec = Z & ( for x being Real st x in Z holds f . x = (sin . x) / ((cos . x) ^2) ) & Z = dom f & f | A is continuous holds integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & dom sec = Z & ( for x being Real st x in Z holds f . x = (sin . x) / ((cos . x) ^2) ) & Z = dom f & f | A is continuous implies integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A)) ) assume that A1: A c= Z and A2: dom sec = Z and A3: for x being Real st x in Z holds f . x = (sin . x) / ((cos . x) ^2) and A4: Z = dom f and A5: f | A is continuous ; ::_thesis: integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A)) A6: sec is_differentiable_on Z by A2, FDIFF_9:4; A7: for x being Real st x in dom (sec `| Z) holds (sec `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom (sec `| Z) implies (sec `| Z) . x = f . x ) assume x in dom (sec `| Z) ; ::_thesis: (sec `| Z) . x = f . x then A8: x in Z by A6, FDIFF_1:def_7; then (sec `| Z) . x = (sin . x) / ((cos . x) ^2) by A2, FDIFF_9:4 .= f . x by A3, A8 ; hence (sec `| Z) . x = f . x ; ::_thesis: verum end; dom (sec `| Z) = dom f by A4, A6, FDIFF_1:def_7; then A9: sec `| Z = f by A7, PARTFUN1:5; ( f is_integrable_on A & f | A is bounded ) by A1, A4, A5, INTEGRA5:10, INTEGRA5:11; hence integral (f,A) = (sec . (upper_bound A)) - (sec . (lower_bound A)) by A1, A2, A9, FDIFF_9:4, INTEGRA5:13; ::_thesis: verum end; theorem Th70: :: INTEGRA9:70 for Z being open Subset of REAL st Z c= dom (- cosec) holds ( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (- cosec) implies ( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) ) ) A1: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; assume A2: Z c= dom (- cosec) ; ::_thesis: ( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) ) then A3: Z c= dom cosec by VALUED_1:8; then for x being Real st x in Z holds sin . x <> 0 by RFUNCT_1:3; then A4: cosec is_differentiable_on Z by A1, FDIFF_2:22; A5: for x being Real st x in Z holds ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) assume A6: x in Z ; ::_thesis: ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) then A7: ( sin . x <> 0 & sin is_differentiable_in x ) by A3, A1, FDIFF_1:9, RFUNCT_1:3; ((- cosec) `| Z) . x = (- 1) * (diff ((sin ^),x)) by A2, A4, A6, FDIFF_1:20 .= (- 1) * (- ((diff (sin,x)) / ((sin . x) ^2))) by A7, FDIFF_2:15 .= (cos . x) / ((sin . x) ^2) by SIN_COS:64 ; hence ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ; ::_thesis: verum end; (- 1) (#) cosec is_differentiable_on Z by A2, A4, FDIFF_1:20; hence ( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) ) ) by A5; ::_thesis: verum end; theorem :: INTEGRA9:71 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 & dom (- cosec) = Z & ( for x being Real st x in Z holds f . x = (cos . x) / ((sin . x) ^2) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- cosec) . (upper_bound A)) - ((- 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 & dom (- cosec) = Z & ( for x being Real st x in Z holds f . x = (cos . x) / ((sin . x) ^2) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A)) let f be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & dom (- cosec) = Z & ( for x being Real st x in Z holds f . x = (cos . x) / ((sin . x) ^2) ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & dom (- cosec) = Z & ( for x being Real st x in Z holds f . x = (cos . x) / ((sin . x) ^2) ) & Z = dom f & f | A is continuous implies integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A)) ) assume that A1: A c= Z and A2: dom (- cosec) = Z and A3: for x being Real st x in Z holds f . x = (cos . x) / ((sin . x) ^2) and A4: Z = dom f and A5: f | A is continuous ; ::_thesis: integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A)) A6: - cosec is_differentiable_on Z by A2, Th70; A7: for x being Real st x in dom ((- cosec) `| Z) holds ((- cosec) `| Z) . x = f . x proof let x be Real; ::_thesis: ( x in dom ((- cosec) `| Z) implies ((- cosec) `| Z) . x = f . x ) assume x in dom ((- cosec) `| Z) ; ::_thesis: ((- cosec) `| Z) . x = f . x then A8: x in Z by A6, FDIFF_1:def_7; then ((- cosec) `| Z) . x = (cos . x) / ((sin . x) ^2) by A2, Th70 .= f . x by A3, A8 ; hence ((- cosec) `| Z) . x = f . x ; ::_thesis: verum end; dom ((- cosec) `| Z) = dom f by A4, A6, FDIFF_1:def_7; then A9: (- cosec) `| Z = f by A7, PARTFUN1:5; ( f is_integrable_on A & f | A is bounded ) by A1, A4, A5, INTEGRA5:10, INTEGRA5:11; hence integral (f,A) = ((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A)) by A1, A2, A9, Th70, INTEGRA5:13; ::_thesis: verum end;