let x, y be PartFunc of REAL,REAL; :: thesis: for Z being open Subset of REAL
for a, b being Real st x is differentiable & y is differentiable & x `| Z is continuous & Z c= dom x & Z c= dom y & a <= b & ['a,b'] c= Z & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) holds
( integral ((y (#) (x `| Z)),a,b) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),a,b) )
let Z be open Subset of REAL; :: thesis: for a, b being Real st x is differentiable & y is differentiable & x `| Z is continuous & Z c= dom x & Z c= dom y & a <= b & ['a,b'] c= Z & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) holds
( integral ((y (#) (x `| Z)),a,b) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),a,b) )
let a, b be Real; :: thesis: ( x is differentiable & y is differentiable & x `| Z is continuous & Z c= dom x & Z c= dom y & a <= b & ['a,b'] c= Z & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) implies ( integral ((y (#) (x `| Z)),a,b) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),a,b) ) )
assume that
A1: ( x is differentiable & y is differentiable ) and
A2: x `| Z is continuous and
A3: ( Z c= dom x & Z c= dom y ) and
A4: ( a <= b & ['a,b'] c= Z ) and
A5: for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ; :: thesis: ( integral ((y (#) (x `| Z)),a,b) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),a,b) )
A6: y | (dom y) is continuous by A1, FDIFF_1:25;
set I = AffineMap (0,1);
A7: dom (AffineMap (0,1)) = REAL by FUNCT_2:def 1;
x is_differentiable_on Z by A1, A3, FDIFF_1:28;
then dom (x `| Z) = Z by FDIFF_1:def 7;
then A11: dom ((x `| Z) (#) (x `| Z)) = Z /\ Z by VALUED_1:def 4
.= Z ;
y is_differentiable_on Z by A1, A3, FDIFF_1:28;
then dom (y `| Z) = Z by FDIFF_1:def 7;
then dom ((y `| Z) (#) (y `| Z)) = Z /\ Z by VALUED_1:def 4
.= Z ;
then A12: dom ((AffineMap (0,1)) - ((y `| Z) (#) (y `| Z))) = REAL /\ Z by A7, VALUED_1:12
.= Z by XBOOLE_1:28 ;
for t being object st t in dom ((x `| Z) (#) (x `| Z)) holds
((x `| Z) (#) (x `| Z)) . t = ((AffineMap (0,1)) - ((y `| Z) (#) (y `| Z))) . t

proof

let t be object ; :: thesis: ( t in dom ((x `| Z) (#) (x `| Z)) implies ((x `| Z) (#) (x `| Z)) . t = ((AffineMap (0,1)) - ((y `| Z) (#) (y `| Z))) . t )
assume A13: t in dom ((x `| Z) (#) (x `| Z)) ; :: thesis: ((x `| Z) (#) (x `| Z)) . t = ((AffineMap (0,1)) - ((y `| Z) (#) (y `| Z))) . t
then reconsider s = t as Real ;
B1: (AffineMap (0,1)) . s = (0 * s) + 1 by FCONT_1:def 4;
(((x `| Z) . s) ^2) + (((y `| Z) . s) ^2) = 1 by A5, A11, A13;
then ((x `| Z) . s) ^2 = 1 - (((y `| Z) . s) ^2)
.= ((AffineMap (0,1)) . s) - (((y `| Z) . s) ^2) by B1 ;
hence ((x `| Z) (#) (x `| Z)) . t = ((AffineMap (0,1)) . s) - (((y `| Z) . s) ^2) by VALUED_1:5
.= ((AffineMap (0,1)) . s) - (((y `| Z) (#) (y `| Z)) . s) by VALUED_1:5
.= ((AffineMap (0,1)) - ((y `| Z) (#) (y `| Z))) . t by A11, A12, A13, VALUED_1:13 ;
:: thesis: verum

end;

then (x `| Z) (#) (x `| Z) = (AffineMap (0,1)) - ((y `| Z) (#) (y `| Z)) by A11, A12, FUNCT_1:2;
hence ( integral ((y (#) (x `| Z)),a,b) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),a,b) ) by A1, A2, A3, A4, A6, Lm10, RFUNCT_1:23; :: thesis: verum