let x, y be PartFunc of REAL,REAL; :: thesis:
let Z be open Subset of REAL; :: thesis:
let u be PartFunc of REAL,REAL; :: thesis:
let G be Real_Sequence; :: thesis:
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 & 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 ) ) ) ; :: thesis:
assume A2: lim G = 0 ; :: thesis:
assume A3: ex t being Real st
( t in ].0,PI.[ & not (u `| ].0,PI.[) . t = 0 ) ; :: thesis:
set g = (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin;
A4: for t being Real holds ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . t = (((u `| ].0,PI.[) . t) * (sin . t)) ^2

proof

end;

A5: for t being Real st t in ].0,PI.[ holds
0 <= ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . t

proof

let t be Real; :: thesis:
((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . t = (((u `| ].0,PI.[) . t) * (sin . t)) ^2 by A4;
hence ( t in ].0,PI.[ implies 0 <= ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . t ) by XREAL_1:63; :: thesis:

end;

consider t0 being Real such that
A6: ( t0 in ].0,PI.[ & (u `| ].0,PI.[) . t0 <> 0 ) by A3;
set t1 = t0 / 2;
A7: ( 0 < t0 & t0 < PI ) by A6, XXREAL_1:4;
then A8: ( 0 < t0 / 2 & t0 / 2 < t0 ) by XREAL_1:216;
A9: 0 < PI - t0 by A7, XREAL_1:50;
set h = (PI - t0) / 2;
reconsider h1 = min ((t0 / 2),((PI - t0) / 2)) as Real ;
A11: ( h1 <= t0 / 2 & h1 <= (PI - t0) / 2 ) by XXREAL_0:17;
A12: 0 < h1 by A7, A9, XXREAL_0:15;
consider n being Nat such that
A13: 1 / h1 < n by SEQ_4:3;
0 + n < n + 1 by XREAL_1:8;
then 1 / h1 < n + 1 by A13, XXREAL_0:2;
then (1 / h1) * h1 <= (n + 1) * h1 by A12, XREAL_1:64;
then 1 <= (n + 1) * h1 by A12, XCMPLX_1:87;
then 1 / (n + 1) <= (h1 * (n + 1)) / (n + 1) by XREAL_1:72;
then A15: 1 / (n + 1) <= h1 by XCMPLX_1:89;
then 1 / (n + 1) <= t0 / 2 by A11, XXREAL_0:2;
then A16: 1 / (n + 1) < t0 by A8, XXREAL_0:2;
A17: (((PI - t0) / 2) + t0) - ((PI - t0) / 2) < PI - ((PI - t0) / 2) by A9, XREAL_1:8;
A18: PI - ((PI - t0) / 2) <= PI - h1 by A11, XREAL_1:13;
PI - h1 <= PI - (1 / (n + 1)) by A15, XREAL_1:13;
then PI - ((PI - t0) / 2) <= PI - (1 / (n + 1)) by A18, XXREAL_0:2;
then t0 < PI - (1 / (n + 1)) by A17, XXREAL_0:2;
then A19: t0 in ].(1 / (n + 1)),(PI - (1 / (n + 1))).[ by A16;
A20: ( 0 < 1 / (n + 1) & 1 / (n + 1) < PI - (1 / (n + 1)) & PI - (1 / (n + 1)) < PI & [.(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;
A21: ].(1 / (n + 1)),(PI - (1 / (n + 1))).[ c= [.(1 / (n + 1)),(PI - (1 / (n + 1))).] by Lm1;
A22: ( ['(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 A1;
sin . t0 <> 0 by A19, A20, A21, COMPTRIG:7;
then (((u `| ].0,PI.[) . t0) * (sin . t0)) ^2 <> 0 by A6;
then 0 <> ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . t0 by A4;
then A25: 0 < ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . t0 by A5, A19, A20, A21;
for t being Real st t in [.(1 / (n + 1)),(PI - (1 / (n + 1))).] holds
0 <= ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) . t by A5, A20;
then consider d, c, e being Real such that
A26: ( 0 < e & c < d & c in [.(1 / (n + 1)),(PI - (1 / (n + 1))).] & d in [.(1 / (n + 1)),(PI - (1 / (n + 1))).] & 0 < e * (d - c) & e * (d - c) <= integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) by A19, A20, A22, A25, Th6;
A27: e * (d - c) <= G . n by A1, A26;
for m being Nat st n <= m holds
e * (d - c) <= G . m

proof

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then G . n <= G . m by A1, A5, Lm25;
hence e * (d - c) <= G . m by A27, XXREAL_0:2; :: thesis:

end;

hence contradiction by A1, A2, A26, Lm2; :: thesis: