theorem :: PDLAX:15

for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL st x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & x `| Z is continuous & y `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 holds
( integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| Z)),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 `| Z)),0,PI) = (1 / 2) * PI ) ) by Lm27, Lm29;