let x, y be PartFunc of REAL,REAL; :: thesis: ( x is differentiable & y is differentiable & ['0,PI'] c= dom x & ['0,PI'] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
((diff (x,t)) ^2) + ((diff (y,t)) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 implies ( integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) implies integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * PI ) ) )
assume A1: ( x is differentiable & y is differentiable & ['0,PI'] c= dom x & ['0,PI'] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
((diff (x,t)) ^2) + ((diff (y,t)) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 ) ; :: thesis: ( integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) implies integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * PI ) )
reconsider Z1 = dom x, Z2 = dom y as open Subset of REAL by A1, FDIFF_1:10;
reconsider Z = Z1 /\ Z2 as open Subset of REAL ;
A3: ( ['0,PI'] c= Z & Z c= dom x & Z c= dom y ) by A1, XBOOLE_1:17, XBOOLE_1:19;
A4: ( x is_differentiable_on Z & y is_differentiable_on Z ) by A1, FDIFF_1:28, XBOOLE_1:17;
A6: ( x `| Z = (x `| (dom x)) | Z & y `| Z = (y `| (dom y)) | Z ) by A1, Th18, XBOOLE_1:17;
A7: for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1

proof

let t be Real; :: thesis: ( t in Z implies (((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 )
assume A8: t in Z ; :: thesis: (((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1
then ( (x `| Z) . t = diff (x,t) & (y `| Z) . t = diff (y,t) ) by A4, FDIFF_1:def 7;
hence (((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 by A1, A8; :: thesis: verum

end;

x `| Z = (x `| (dom x)) | Z by A1, Th18, XBOOLE_1:17;
then A11: y (#) (x `| Z) = (y (#) (x `| (dom x))) | Z by RFUNCT_1:45;
integral ((y (#) (x `| Z)),0,PI) = integral ((y (#) (x `| Z)),['0,PI']) by INTEGRA5:def 4, LmPI
.= integral ((y (#) (x `| (dom x))),['0,PI']) by A1, A11, RELAT_1:74, XBOOLE_1:19
.= integral ((y (#) (x `| (dom x))),0,PI) by INTEGRA5:def 4, LmPI ;
hence ( integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) implies integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * PI ) ) by A1, A3, A6, A7, Lm27, Lm29; :: thesis: verum