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 G 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)) ) & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous & dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
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 G 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)) ) & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous & dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI ) )
assume ( 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 G 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)) ) & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous & dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
then consider u being PartFunc of REAL,REAL, F being Real_Sequence such that
A1: ( 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 Th20;
set I = AffineMap (0,1);
AA: dom (AffineMap (0,1)) = REAL by FUNCT_2:def 1;
(AffineMap (0,1)) | ['0,PI'] is continuous ;
then consider NI being Real_Sequence such that
A4: ( ( for n being Nat holds NI . n = integral ((AffineMap (0,1)),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) ) & NI is convergent & lim NI = integral ((AffineMap (0,1)),0,PI) ) by AA, Th7, LEIBNIZ1:17;
for t being Real st t in ['0,PI'] holds
(AffineMap (0,1)) . t = 1

proof

let t be Real; :: thesis: ( t in ['0,PI'] implies (AffineMap (0,1)) . t = 1 )
(AffineMap (0,1)) . t = (0 * t) + 1 by FCONT_1:def 4
.= 1 ;
hence ( t in ['0,PI'] implies (AffineMap (0,1)) . t = 1 ) ; :: thesis: verum

end;

then A5: lim NI = 1 * (PI - 0) by AA, A4, INTEGRA6:26, LmPI
.= PI ;
deffunc H₁( Nat) -> Element of REAL = In ((integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / ($1 + 1)),(PI - (1 / ($1 + 1))))),REAL);
consider G being Function of NAT,REAL such that
A6: for x being Element of NAT holds G . x = H₁(x) from FUNCT_2:sch 4();
take u ; :: thesis: ex G 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)) ) & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous & dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
take G ; :: 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)) ) & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous & dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
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)) ) ) by A1; :: thesis: ( (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous & dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
set GN = (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin;
thus (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous by A1; :: thesis: ( dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
dom (u `| ].0,PI.[) = ].0,PI.[ by A1, FDIFF_1:def 7;
then A8: dom ((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) = ].0,PI.[ /\ ].0,PI.[ by VALUED_1:def 4
.= ].0,PI.[ ;
A9: dom sin = REAL by FUNCT_2:def 1;
then dom (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) = ].0,PI.[ /\ REAL by A8, VALUED_1:def 4
.= ].0,PI.[ by XBOOLE_1:28 ;
hence A10: dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ /\ REAL by A9, VALUED_1:def 4
.= ].0,PI.[ by XBOOLE_1:28 ;
:: thesis: ( ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
thus A11: for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) :: thesis: ( G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )

proof

let n be Nat; :: thesis: G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1))))
n in NAT by ORDINAL1:def 12;
hence G . n = In ((integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1))))),REAL) by A6
.= integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ;
:: thesis: verum

end;

A12: for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] & G . n = (NI . n) + ((- F) . n) )

proof

let n be Nat; :: thesis: ( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] & G . n = (NI . n) + ((- F) . n) )
A13: NI . n = integral ((AffineMap (0,1)),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) by A4
.= integral ((AffineMap (0,1)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ;
A14: ( 0 < 1 / (n + 1) & 1 / (n + 1) < PI - (1 / (n + 1)) & [.(1 / (n + 1)),(PI - (1 / (n + 1))).] c= ].0,PI.[ & ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).] ) by Lm3;
set Z = ['(1 / (n + 1)),(PI - (1 / (n + 1)))'];
thus ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) by A10, A14; :: thesis: ( ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] & G . n = (NI . n) + ((- F) . n) )
thus ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous by A1; :: thesis: ( ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] & G . n = (NI . n) + ((- F) . n) )
hence A16: ( ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) by A10, A14, INTEGRA5:10, INTEGRA5:11; :: thesis: G . n = (NI . n) + ((- F) . n)
for t being Real st t in ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] holds
(AffineMap (0,1)) . t = 1

proof

let t be Real; :: thesis: ( t in ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] implies (AffineMap (0,1)) . t = 1 )
(AffineMap (0,1)) . t = (0 * t) + 1 by FCONT_1:def 4
.= 1 ;
hence ( t in ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] implies (AffineMap (0,1)) . t = 1 ) ; :: thesis: verum

end;

then A18: ( (AffineMap (0,1)) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & AffineMap (0,1) is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] & integral ((AffineMap (0,1)),(1 / (n + 1)),(PI - (1 / (n + 1)))) = 1 * ((PI - (1 / (n + 1))) - (1 / (n + 1))) ) by AA, A14, INTEGRA6:26;
F . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) by A1
.= (NI . n) - (integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1))))) by AA, A10, A13, A14, A16, A18, INTEGRA6:12
.= (NI . n) - (G . n) by A11 ;
hence G . n = (NI . n) - (F . n)
.= (NI . n) + ((- F) . n) by SEQ_1:10 ;
:: thesis: verum

end;

then A19: G = NI - F by SEQ_1:7;
thus G is convergent by A1, A4, A19; :: thesis: ( ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
A21: lim G = (lim NI) - (lim F) by A1, A4, A19, SEQ_2:12;
thus for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) by A12; :: thesis: ( ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
set ZZ = REAL --> 0;
A23: dom (REAL --> 0) = REAL by FUNCOP_1:13;
rng (REAL --> 0) c= REAL ;
then reconsider ZZ = REAL --> 0 as PartFunc of REAL,REAL by A23, RELSET_1:4;
thus A25: for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) :: thesis: ( 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) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )

proof

let n be Nat; :: thesis: ( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI )
set GnF = (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin;
set Z = ['(1 / (n + 1)),(PI - (1 / (n + 1)))'];
A26: ( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) by A12;
A27: ( 0 < 1 / (n + 1) & 1 / (n + 1) < PI - (1 / (n + 1)) & [.(1 / (n + 1)),(PI - (1 / (n + 1))).] c= ].0,PI.[ & ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).] ) by Lm3;
A28: for t being Real st t in ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] holds
ZZ . t = 0 by FUNCOP_1:7;
A30: ( ZZ is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] & ZZ | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & integral (ZZ,(1 / (n + 1)),(PI - (1 / (n + 1)))) = 0 * ((PI - (1 / (n + 1))) - (1 / (n + 1))) ) by A23, A27, A28, INTEGRA6:26;
for x being Real st x in ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] holds
ZZ . x <= ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . x

proof

let x be Real; :: thesis: ( x in ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] implies ZZ . x <= ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . x )
assume x in ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ; :: thesis: ZZ . x <= ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . x
then A31: ZZ . x = 0 by FUNCOP_1:7;
A32: ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . x = ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) . x) * (sin . x) by VALUED_1:5
.= ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) . x) * (sin . x)) * (sin . x) by VALUED_1:5
.= ((((u `| ].0,PI.[) . x) ^2) * (sin . x)) * (sin . x) by VALUED_1:5
.= (((u `| ].0,PI.[) . x) ^2) * ((sin . x) ^2) ;
( 0 <= ((u `| ].0,PI.[) . x) ^2 & 0 <= (sin . x) ^2 ) by XREAL_1:63;
hence ZZ . x <= ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . x by A31, A32; :: thesis: verum

end;

then integral (ZZ,(1 / (n + 1)),(PI - (1 / (n + 1)))) <= integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) by A23, A26, A27, A30, ORDEQ_01:48;
hence 0 <= G . n by A11, A30; :: thesis: ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI
then ((1 / 2) * PI) - (G . n) <= ((1 / 2) * PI) - 0 by XREAL_1:13;
hence ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ; :: thesis: verum

end;

thus ( 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; :: thesis: ( (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
thus (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) by A1, A5, A21; :: thesis: ( 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )
consider S310 being constant Function of NAT,REAL such that
A36: for x being Nat holds S310 . x = 0 by LmX;
S310 . 0 = 0 by A36;
then A39: ( S310 is convergent & lim S310 = 0 ) by SEQ_4:25;
for n being Nat holds S310 . n <= G . n

proof

let n be Nat; :: thesis: S310 . n <= G . n
S310 . n = 0 by A36;
hence S310 . n <= G . n by A25; :: thesis: verum

end;

hence 0 <= lim G by A1, A4, A19, A39, SEQ_2:18; :: thesis: ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI
then ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= ((1 / 2) * PI) - 0 by XREAL_1:13;
hence ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI ; :: thesis: verum