let a be Real; for A being non empty closed_interval Subset of REAL
for f, f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (tan * f1) & f = ((sin * f1) ^2) / ((cos * f1) ^2) & ( for x being Real st x in Z holds
( f1 . x = a * x & a <> 0 ) ) & Z = dom f holds
integral (f,A) = ((((1 / a) (#) (tan * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (tan * f1)) - (id Z)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; for f, f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (tan * f1) & f = ((sin * f1) ^2) / ((cos * f1) ^2) & ( for x being Real st x in Z holds
( f1 . x = a * x & a <> 0 ) ) & Z = dom f holds
integral (f,A) = ((((1 / a) (#) (tan * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (tan * f1)) - (id Z)) . (lower_bound A))
let f, f1 be PartFunc of REAL,REAL; for Z being open Subset of REAL st A c= Z & Z c= dom (tan * f1) & f = ((sin * f1) ^2) / ((cos * f1) ^2) & ( for x being Real st x in Z holds
( f1 . x = a * x & a <> 0 ) ) & Z = dom f holds
integral (f,A) = ((((1 / a) (#) (tan * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (tan * f1)) - (id Z)) . (lower_bound A))
let Z be open Subset of REAL; ( A c= Z & Z c= dom (tan * f1) & f = ((sin * f1) ^2) / ((cos * f1) ^2) & ( for x being Real st x in Z holds
( f1 . x = a * x & a <> 0 ) ) & Z = dom f implies integral (f,A) = ((((1 / a) (#) (tan * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (tan * f1)) - (id Z)) . (lower_bound A)) )
assume A1:
( A c= Z & Z c= dom (tan * f1) & f = ((sin * f1) ^2) / ((cos * f1) ^2) & ( for x being Real st x in Z holds
( f1 . x = a * x & a <> 0 ) ) & Z = dom f )
; integral (f,A) = ((((1 / a) (#) (tan * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (tan * f1)) - (id Z)) . (lower_bound A))
then A2:
Z c= dom ((1 / a) (#) (tan * f1))
by VALUED_1:def 5;
Z c= (dom ((1 / a) (#) (tan * f1))) /\ (dom (id Z))
by A2, XBOOLE_1:19;
then A3:
Z c= dom (((1 / a) (#) (tan * f1)) - (id Z))
by VALUED_1:12;
A4:
for x being Real st x in Z holds
f1 . x = (a * x) + 0
by A1;
Z = (dom ((sin * f1) ^2)) /\ ((dom ((cos * f1) ^2)) \ (((cos * f1) ^2) " {0}))
by A1, RFUNCT_1:def 1;
then A5:
( Z c= dom ((sin * f1) ^2) & Z c= (dom ((cos * f1) ^2)) \ (((cos * f1) ^2) " {0}) )
by XBOOLE_1:18;
then A6:
Z c= dom (sin * f1)
by VALUED_1:11;
A7:
Z c= dom (((cos * f1) ^2) ^)
by A5, RFUNCT_1:def 2;
dom (((cos * f1) ^2) ^) c= dom ((cos * f1) ^2)
by RFUNCT_1:1;
then
Z c= dom ((cos * f1) ^2)
by A7;
then A8:
Z c= dom (cos * f1)
by VALUED_1:11;
A9:
sin * f1 is_differentiable_on Z
by A6, A4, FDIFF_4:37;
A10:
cos * f1 is_differentiable_on Z
by A4, A8, FDIFF_4:38;
A11:
(sin * f1) ^2 is_differentiable_on Z
by A9, FDIFF_2:20;
A12:
(cos * f1) ^2 is_differentiable_on Z
by A10, FDIFF_2:20;
for x being Real st x in Z holds
((cos * f1) ^2) . x <> 0
then
f is_differentiable_on Z
by A1, A11, A12, FDIFF_2:21;
then
f | Z is continuous
by FDIFF_1:25;
then
f | A is continuous
by A1, FCONT_1:16;
then A13:
( f is_integrable_on A & f | A is bounded )
by A1, INTEGRA5:10, INTEGRA5:11;
A14:
((1 / a) (#) (tan * f1)) - (id Z) is_differentiable_on Z
by A1, A3, FDIFF_8:26;
A15:
for x being Real st x in Z holds
f . x = ((sin . (a * x)) ^2) / ((cos . (a * x)) ^2)
A17:
for x being Element of REAL st x in dom ((((1 / a) (#) (tan * f1)) - (id Z)) `| Z) holds
((((1 / a) (#) (tan * f1)) - (id Z)) `| Z) . x = f . x
dom ((((1 / a) (#) (tan * f1)) - (id Z)) `| Z) = dom f
by A1, A14, FDIFF_1:def 7;
then
(((1 / a) (#) (tan * f1)) - (id Z)) `| Z = f
by A17, PARTFUN1:5;
hence
integral (f,A) = ((((1 / a) (#) (tan * f1)) - (id Z)) . (upper_bound A)) - ((((1 / a) (#) (tan * f1)) - (id Z)) . (lower_bound A))
by A1, A13, A14, INTEGRA5:13; verum