let x, y be PartFunc of REAL,REAL; :: thesis: for Z being open Subset of REAL
for a, b being Real st x is continuous & y is differentiable & y `| Z is continuous & a <= b & ['a,b'] c= Z & Z c= dom x & Z c= dom y holds
integral ((x (#) (y `| Z)),a,b) <= (1 / 2) * (integral (((x (#) x) + ((y `| Z) (#) (y `| Z))),a,b))
let Z be open Subset of REAL; :: thesis: for a, b being Real st x is continuous & y is differentiable & y `| Z is continuous & a <= b & ['a,b'] c= Z & Z c= dom x & Z c= dom y holds
integral ((x (#) (y `| Z)),a,b) <= (1 / 2) * (integral (((x (#) x) + ((y `| Z) (#) (y `| Z))),a,b))
let a, b be Real; :: thesis: ( x is continuous & y is differentiable & y `| Z is continuous & a <= b & ['a,b'] c= Z & Z c= dom x & Z c= dom y implies integral ((x (#) (y `| Z)),a,b) <= (1 / 2) * (integral (((x (#) x) + ((y `| Z) (#) (y `| Z))),a,b)) )
assume that
A1: x is continuous and
A2: y is differentiable and
A3: y `| Z is continuous and
A4: ( a <= b & ['a,b'] c= Z & Z c= dom x & Z c= dom y ) ; :: thesis: integral ((x (#) (y `| Z)),a,b) <= (1 / 2) * (integral (((x (#) x) + ((y `| Z) (#) (y `| Z))),a,b))
A5: (x (#) (y `| Z)) | ['a,b'] is continuous by A1, A3;
y is_differentiable_on Z by A2, A4, FDIFF_1:28;
then A6: dom (y `| Z) = Z by FDIFF_1:def 7;
then A7: dom (x (#) (y `| Z)) = (dom x) /\ Z by VALUED_1:def 4
.= Z by A4, XBOOLE_1:28 ;
A9: ((1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)))) | ['a,b'] is continuous by A1, A3;
A10: ((x (#) x) + ((y `| Z) (#) (y `| Z))) | ['a,b'] is continuous by A1, A3;
A11: dom ((x (#) x) + ((y `| Z) (#) (y `| Z))) = (dom (x (#) x)) /\ (dom ((y `| Z) (#) (y `| Z))) by VALUED_1:def 1
.= ((dom x) /\ (dom x)) /\ (dom ((y `| Z) (#) (y `| Z))) by VALUED_1:def 4
.= (dom x) /\ (Z /\ Z) by A6, VALUED_1:def 4
.= Z by A4, XBOOLE_1:28 ;
then A12: dom ((1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)))) = Z by VALUED_1:def 5;
set f = x (#) (y `| Z);
set g0 = (x (#) x) + ((y `| Z) (#) (y `| Z));
set g = (1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)));
A13: ( (x (#) (y `| Z)) | ['a,b'] is bounded & x (#) (y `| Z) is_integrable_on ['a,b'] ) by A4, A5, A7, INTEGRA5:10, INTEGRA5:11;
A14: ( ((1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)))) | ['a,b'] is bounded & (1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z))) is_integrable_on ['a,b'] ) by A4, A9, A12, INTEGRA5:10, INTEGRA5:11;
A15: ( ((x (#) x) + ((y `| Z) (#) (y `| Z))) | ['a,b'] is bounded & (x (#) x) + ((y `| Z) (#) (y `| Z)) is_integrable_on ['a,b'] ) by A4, A10, A11, INTEGRA5:10, INTEGRA5:11;
for t being Real st t in ['a,b'] holds
(x (#) (y `| Z)) . t <= ((1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)))) . t

proof

let t be Real; :: thesis: ( t in ['a,b'] implies (x (#) (y `| Z)) . t <= ((1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)))) . t )
assume A16: t in ['a,b'] ; :: thesis: (x (#) (y `| Z)) . t <= ((1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)))) . t
((1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)))) . t = (1 / 2) * (((x (#) x) + ((y `| Z) (#) (y `| Z))) . t) by VALUED_1:6
.= (1 / 2) * (((x (#) x) . t) + (((y `| Z) (#) (y `| Z)) . t)) by A4, A11, A16, VALUED_1:def 1 ;
hence (x (#) (y `| Z)) . t <= ((1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)))) . t by Lm7; :: thesis: verum

end;

then integral ((x (#) (y `| Z)),a,b) <= integral (((1 / 2) (#) ((x (#) x) + ((y `| Z) (#) (y `| Z)))),a,b) by A4, A7, A12, A13, A14, ORDEQ_01:48;
hence integral ((x (#) (y `| Z)),a,b) <= (1 / 2) * (integral (((x (#) x) + ((y `| Z) (#) (y `| Z))),a,b)) by A4, A11, A15, INTEGRA6:10; :: thesis: verum