theorem Th22: :: PDLAX:16

for x, y being PartFunc of REAL,REAL st 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 holds
( 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 ) )