let x, y be PartFunc of REAL,REAL; :: thesis: 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 )
let Z be open Subset of REAL; :: thesis: ( 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 implies 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 ) )
assume A1: ( 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 ) ; :: thesis: 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 )
set I = AffineMap (0,1);
A3: ( 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) ) by A1, Lm11, LEIBNIZ1:17;
consider u being PartFunc of REAL,REAL such that
A4: ( dom u = ['0,PI'] & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & 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)) ) ) by A1, Lm17;
consider F being Real_Sequence such that
A5: ( ( 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 (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI) = lim F ) by A1, A4, Lm21;
take u ; :: thesis: 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 )
take F ; :: thesis: ( 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 )
thus ( 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 ) by A3, A4, A5; :: thesis: verum