let A be non empty closed_interval Subset of REAL; :: thesis: for f, g being PartFunc of REAL,REAL

for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds

integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))

let f, g be PartFunc of REAL,REAL; :: thesis: for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds

integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))

let X be open Subset of REAL; :: thesis: ( f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded implies integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) )

assume that

A1: f is_differentiable_on X and

A2: g is_differentiable_on X and

A3: A c= X and

A4: f `| X is_integrable_on A and

A5: (f `| X) | A is bounded and

A6: g `| X is_integrable_on A and

A7: (g `| X) | A is bounded ; :: thesis: integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))

A8: (f (#) g) `| X = ((f `| X) (#) g) + (f (#) (g `| X)) by A1, A2, FDIFF_2:20;

g | X is continuous by A2, FDIFF_1:25;

then A9: g | A is continuous by A3, FCONT_1:16;

X c= dom g by A2, FDIFF_1:def 6;

then A10: A c= dom g by A3, XBOOLE_1:1;

then A11: g || A is Function of A,REAL by Th6, FUNCT_2:68;

X c= dom g by A2, FDIFF_1:def 6;

then g is_integrable_on A by A3, A9, Th11, XBOOLE_1:1;

then A12: g || A is integrable ;

A13: A c= dom (g `| X) by A2, A3, FDIFF_1:def 7;

then A14: (g `| X) || A is Function of A,REAL by Th6, FUNCT_2:68;

g | X is continuous by A2, FDIFF_1:25;

then g | A is bounded by A3, A10, Th10, FCONT_1:16;

then A15: ((f `| X) (#) g) | (A /\ A) is bounded by A5, RFUNCT_1:84;

then A16: (((f `| X) (#) g) || A) | A is bounded ;

f | X is continuous by A1, FDIFF_1:25;

then A17: f | A is continuous by A3, FCONT_1:16;

X c= dom f by A1, FDIFF_1:def 6;

then f is_integrable_on A by A3, A17, Th11, XBOOLE_1:1;

then A18: f || A is integrable ;

A19: A c= dom (f `| X) by A1, A3, FDIFF_1:def 7;

then A20: (f `| X) || A is Function of A,REAL by Th6, FUNCT_2:68;

A21: ( (g `| X) || A is integrable & ((g `| X) || A) | A is bounded ) by A6, A7;

A22: ( (f `| X) || A is integrable & ((f `| X) || A) | A is bounded ) by A4, A5;

dom ((f `| X) (#) g) = (dom (f `| X)) /\ (dom g) by VALUED_1:def 4;

then A c= dom ((f `| X) (#) g) by A10, A19, XBOOLE_1:19;

then A23: ((f `| X) (#) g) || A is Function of A,REAL by Th6, FUNCT_2:68;

X c= dom f by A1, FDIFF_1:def 6;

then A24: A c= dom f by A3, XBOOLE_1:1;

then A25: f || A is Function of A,REAL by Th6, FUNCT_2:68;

f | X is continuous by A1, FDIFF_1:25;

then f | A is bounded by A3, A24, Th10, FCONT_1:16;

then A26: (f (#) (g `| X)) | (A /\ A) is bounded by A7, RFUNCT_1:84;

then A27: ((f (#) (g `| X)) || A) | A is bounded ;

(((f `| X) (#) g) + (f (#) (g `| X))) | (A /\ A) is bounded by A15, A26, RFUNCT_1:83;

then A28: ((f (#) g) `| X) | A is bounded by A1, A2, FDIFF_2:20;

A29: ( (f (#) g) . (upper_bound A) = (f . (upper_bound A)) * (g . (upper_bound A)) & (f (#) g) . (lower_bound A) = (f . (lower_bound A)) * (g . (lower_bound A)) ) by VALUED_1:5;

dom (f (#) (g `| X)) = (dom f) /\ (dom (g `| X)) by VALUED_1:def 4;

then A c= dom (f (#) (g `| X)) by A24, A13, XBOOLE_1:19;

then A30: (f (#) (g `| X)) || A is Function of A,REAL by Th6, FUNCT_2:68;

(g || A) | A is bounded by A9, A10, Th10;

then ((f `| X) || A) (#) (g || A) is integrable by A12, A11, A20, A22, INTEGRA4:29;

then A31: ((f `| X) (#) g) || A is integrable by Th4;

(f || A) | A is bounded by A17, A24, Th10;

then (f || A) (#) ((g `| X) || A) is integrable by A18, A25, A14, A21, INTEGRA4:29;

then A32: (f (#) (g `| X)) || A is integrable by Th4;

then integral ((((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A)) = (integral (((f `| X) (#) g) || A)) + (integral ((f (#) (g `| X)) || A)) by A31, A23, A16, A30, A27, INTEGRA1:57;

then A33: integral ((((f `| X) (#) g) + (f (#) (g `| X))) || A) = (integral (((f `| X) (#) g),A)) + (integral ((f (#) (g `| X)),A)) by Th5;

(((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A) is integrable by A31, A32, A23, A16, A30, A27, INTEGRA1:57;

then (((f `| X) (#) g) + (f (#) (g `| X))) || A is integrable by Th5;

then A34: (f (#) g) `| X is_integrable_on A by A8;

integral (((f (#) g) `| X) || A) = integral (((f (#) g) `| X),A)

.= ((f (#) g) . (upper_bound A)) - ((f (#) g) . (lower_bound A)) by A1, A2, A3, A34, A28, Th13, FDIFF_2:20 ;

hence integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) by A8, A29, A33; :: thesis: verum

for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds

integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))

let f, g be PartFunc of REAL,REAL; :: thesis: for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds

integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))

let X be open Subset of REAL; :: thesis: ( f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded implies integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) )

assume that

A1: f is_differentiable_on X and

A2: g is_differentiable_on X and

A3: A c= X and

A4: f `| X is_integrable_on A and

A5: (f `| X) | A is bounded and

A6: g `| X is_integrable_on A and

A7: (g `| X) | A is bounded ; :: thesis: integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))

A8: (f (#) g) `| X = ((f `| X) (#) g) + (f (#) (g `| X)) by A1, A2, FDIFF_2:20;

g | X is continuous by A2, FDIFF_1:25;

then A9: g | A is continuous by A3, FCONT_1:16;

X c= dom g by A2, FDIFF_1:def 6;

then A10: A c= dom g by A3, XBOOLE_1:1;

then A11: g || A is Function of A,REAL by Th6, FUNCT_2:68;

X c= dom g by A2, FDIFF_1:def 6;

then g is_integrable_on A by A3, A9, Th11, XBOOLE_1:1;

then A12: g || A is integrable ;

A13: A c= dom (g `| X) by A2, A3, FDIFF_1:def 7;

then A14: (g `| X) || A is Function of A,REAL by Th6, FUNCT_2:68;

g | X is continuous by A2, FDIFF_1:25;

then g | A is bounded by A3, A10, Th10, FCONT_1:16;

then A15: ((f `| X) (#) g) | (A /\ A) is bounded by A5, RFUNCT_1:84;

then A16: (((f `| X) (#) g) || A) | A is bounded ;

f | X is continuous by A1, FDIFF_1:25;

then A17: f | A is continuous by A3, FCONT_1:16;

X c= dom f by A1, FDIFF_1:def 6;

then f is_integrable_on A by A3, A17, Th11, XBOOLE_1:1;

then A18: f || A is integrable ;

A19: A c= dom (f `| X) by A1, A3, FDIFF_1:def 7;

then A20: (f `| X) || A is Function of A,REAL by Th6, FUNCT_2:68;

A21: ( (g `| X) || A is integrable & ((g `| X) || A) | A is bounded ) by A6, A7;

A22: ( (f `| X) || A is integrable & ((f `| X) || A) | A is bounded ) by A4, A5;

dom ((f `| X) (#) g) = (dom (f `| X)) /\ (dom g) by VALUED_1:def 4;

then A c= dom ((f `| X) (#) g) by A10, A19, XBOOLE_1:19;

then A23: ((f `| X) (#) g) || A is Function of A,REAL by Th6, FUNCT_2:68;

X c= dom f by A1, FDIFF_1:def 6;

then A24: A c= dom f by A3, XBOOLE_1:1;

then A25: f || A is Function of A,REAL by Th6, FUNCT_2:68;

f | X is continuous by A1, FDIFF_1:25;

then f | A is bounded by A3, A24, Th10, FCONT_1:16;

then A26: (f (#) (g `| X)) | (A /\ A) is bounded by A7, RFUNCT_1:84;

then A27: ((f (#) (g `| X)) || A) | A is bounded ;

(((f `| X) (#) g) + (f (#) (g `| X))) | (A /\ A) is bounded by A15, A26, RFUNCT_1:83;

then A28: ((f (#) g) `| X) | A is bounded by A1, A2, FDIFF_2:20;

A29: ( (f (#) g) . (upper_bound A) = (f . (upper_bound A)) * (g . (upper_bound A)) & (f (#) g) . (lower_bound A) = (f . (lower_bound A)) * (g . (lower_bound A)) ) by VALUED_1:5;

dom (f (#) (g `| X)) = (dom f) /\ (dom (g `| X)) by VALUED_1:def 4;

then A c= dom (f (#) (g `| X)) by A24, A13, XBOOLE_1:19;

then A30: (f (#) (g `| X)) || A is Function of A,REAL by Th6, FUNCT_2:68;

(g || A) | A is bounded by A9, A10, Th10;

then ((f `| X) || A) (#) (g || A) is integrable by A12, A11, A20, A22, INTEGRA4:29;

then A31: ((f `| X) (#) g) || A is integrable by Th4;

(f || A) | A is bounded by A17, A24, Th10;

then (f || A) (#) ((g `| X) || A) is integrable by A18, A25, A14, A21, INTEGRA4:29;

then A32: (f (#) (g `| X)) || A is integrable by Th4;

then integral ((((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A)) = (integral (((f `| X) (#) g) || A)) + (integral ((f (#) (g `| X)) || A)) by A31, A23, A16, A30, A27, INTEGRA1:57;

then A33: integral ((((f `| X) (#) g) + (f (#) (g `| X))) || A) = (integral (((f `| X) (#) g),A)) + (integral ((f (#) (g `| X)),A)) by Th5;

(((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A) is integrable by A31, A32, A23, A16, A30, A27, INTEGRA1:57;

then (((f `| X) (#) g) + (f (#) (g `| X))) || A is integrable by Th5;

then A34: (f (#) g) `| X is_integrable_on A by A8;

integral (((f (#) g) `| X) || A) = integral (((f (#) g) `| X),A)

.= ((f (#) g) . (upper_bound A)) - ((f (#) g) . (lower_bound A)) by A1, A2, A3, A34, A28, Th13, FDIFF_2:20 ;

hence integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) by A8, A29, A33; :: thesis: verum