theorem Th20: :: PDLAX:14

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 & y `| Z is continuous & x `| 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
ex u being PartFunc of REAL,REAL ex F being Real_Sequence st
( u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) & ( for n being Nat holds F . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & F is convergent & integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI) & integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI) = lim F )