let y be PartFunc of REAL,REAL; :: thesis:
let Z be open Subset of REAL; :: thesis:
assume A1: ( ['0,PI'] c= Z & Z c= dom y & y is differentiable & y `| Z is continuous & y . 0 = 0 & y . PI = 0 ) ; :: thesis:
A3: ['0,PI'] = [.0,PI.] by INTEGRA5:def 3, LmPI;
then A4: ].0,PI.[ c= ['0,PI'] by Lm1;
then A5: ].0,PI.[ c= Z by A1;
A6: ].0,PI.[ c= dom y by A1, A4;
A7: y is_differentiable_on Z by A1, FDIFF_1:26;
then A10: y is_differentiable_on ].0,PI.[ by A5, FDIFF_1:26;
A9: ['0,PI'] c= dom y by A1;
A11: for t being Real st t in ].0,PI.[ holds
( y / sin is_differentiable_in t & diff ((y / sin),t) = (((diff (y,t)) * (sin . t)) - ((diff (sin,t)) * (y . t))) / ((sin . t) ^2) )

proof

let t be Real; :: thesis:
assume A12: t in ].0,PI.[ ; :: thesis:
then A13: 0 < sin . t by COMPTRIG:7;
A14: ( sin is_differentiable_in t & diff (sin,t) = cos . t ) by SIN_COS:64;
A15: y is_differentiable_on dom y by A1;
t in dom y by A1, A4, A12;
then y is_differentiable_in t by A15;
hence ( y / sin is_differentiable_in t & diff ((y / sin),t) = (((diff (y,t)) * (sin . t)) - ((diff (sin,t)) * (y . t))) / ((sin . t) ^2) ) by A13, A14, FDIFF_2:14; :: thesis:

end;

B15: now :: thesis:

let t be object ; :: thesis:
assume A16: t in ].0,PI.[ ; :: thesis:
then reconsider s = t as Real ;
A17: dom sin = REAL by FUNCT_2:def 1;
A18: s in REAL by XREAL_0:def 1;
A19: sin . s <> 0 by A16, COMPTRIG:7;
not s in sin " {0}

proof

assume s in sin " {0} ; :: thesis:
then ( s in dom sin & sin . s in {0} ) by FUNCT_1:def 7;
hence contradiction by A19, TARSKI:def 1; :: thesis:

end;

then s in (dom sin) \ (sin " {0}) by A17, A18, XBOOLE_0:def 5;
then t in (dom y) /\ ((dom sin) \ (sin " {0})) by A6, A16, XBOOLE_0:def 4;
hence t in dom (y / sin) by RFUNCT_1:def 1; :: thesis:

end;

then A21: ].0,PI.[ c= dom (y / sin) ;
A22: for t being Real st t in ].0,PI.[ holds
y / sin is_continuous_in t by A11, FDIFF_1:24;
defpred S₁[ object ] means $1 in ].0,PI.[;
deffunc H₁( object ) -> set = (y / sin) . $1;
deffunc H₂( object ) -> set = (diff (y,(In ($1,REAL)))) * (cos . (In ($1,REAL)));
consider u being Function such that
A23: ( dom u = ['0,PI'] & ( for x being set st x in ['0,PI'] holds
( ( S₁[x] implies u . x = H₁(x) ) & ( not S₁[x] implies u . x = H₂(x) ) ) ) ) from PARTFUN1:sch 5();
A24: for t being Real holds
( ( t in ].0,PI.[ implies u . t = (y / sin) . t ) & ( t = 0 implies u . t = diff (y,t) ) & ( t = PI implies u . t = - (diff (y,t)) ) )

proof

let t be Real; :: thesis:
A0: ].0,PI.[ c= [.0,PI.] by Lm1;
thus ( t in ].0,PI.[ implies u . t = (y / sin) . t ) by A0, A3, A23; :: thesis:
thus ( t = 0 implies u . t = diff (y,t) ) :: thesis:

proof

assume A26: t = 0 ; :: thesis:
then A25: t in ['0,PI'] by A3, LmPI;
not t in ].0,PI.[ by A26, XXREAL_1:4;
hence u . t = (diff (y,t)) * (cos . (In (t,REAL))) by A23, A25
.= diff (y,t) by A26, SIN_COS:30 ;
:: thesis:

end;

thus ( t = PI implies u . t = - (diff (y,t)) ) :: thesis:

proof

assume A27: t = PI ; :: thesis:
then A25: t in ['0,PI'] by A3, LmPI;
not t in ].0,PI.[ by A27, XXREAL_1:4;
hence u . t = (diff (y,t)) * (cos . (In (t,REAL))) by A23, A25
.= - (diff (y,t)) by A27, SIN_COS:76 ;
:: thesis:

end;

rng u c= REAL

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng u ; :: thesis:
then consider t being object such that
A28: ( t in dom u & z = u . t ) by FUNCT_1:def 3;
reconsider t = t as Real by A23, A28;
ex r being Real st
( r = t & 0 <= r & r <= PI ) by A3, A23, A28;
then ( 0 = t or ( 0 < t & t < PI ) or t = PI ) by XXREAL_0:1;

per cases ;

suppose ( 0 = t or t = PI ) ; :: thesis:

then ( u . t = diff (y,t) or u . t = - (diff (y,t)) ) by A24;
hence z in REAL by A28, XREAL_0:def 1; :: thesis:

end;

suppose t in ].0,PI.[ ; :: thesis:

then u . t = (y / sin) . t by A23, A28;
hence z in REAL by A28, XREAL_0:def 1; :: thesis:

end;

then reconsider u = u as PartFunc of REAL,REAL by A23, RELSET_1:4;
A31: dom (u | ].0,PI.[) = ].0,PI.[ by A4, A23, RELAT_1:62;
A32: dom ((y / sin) | ].0,PI.[) = ].0,PI.[ by A21, RELAT_1:62;
B32: for t being object st t in dom (u | ].0,PI.[) holds
(u | ].0,PI.[) . t = ((y / sin) | ].0,PI.[) . t

proof

let t be object ; :: thesis:
assume A33: t in dom (u | ].0,PI.[) ; :: thesis:
hence (u | ].0,PI.[) . t = u . t by A31, FUNCT_1:49
.= (y / sin) . t by A4, A23, A31, A33
.= ((y / sin) | ].0,PI.[) . t by A31, A33, FUNCT_1:49 ;
:: thesis:

end;

then A35: u | ].0,PI.[ = (y / sin) | ].0,PI.[ by A31, A32, FUNCT_1:2;
for t being Real st t in dom u holds
u is_continuous_in t

proof

let t be Real; :: thesis:
assume A36: t in dom u ; :: thesis:
then ( 0 <= t & t <= PI ) by A3, A23, XXREAL_1:1;

per cases by XXREAL_0:1;

suppose A38: ( 0 < t & t < PI ) ; :: thesis:

then A39: t in ].0,PI.[ ;

now :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s1 being Real such that
A41: ( 0 < s1 & ( for t1 being Real st t1 in dom (y / sin) & |.(t1 - t).| < s1 holds
|.(((y / sin) . t1) - ((y / sin) . t)).| < r ) ) by A22, A39, FCONT_1:3;
set s20 = (PI - t) / 2;
set s21 = t / 2;
A44: ( 0 < t / 2 & t / 2 < t ) by A38, XREAL_1:216;
reconsider s2 = min (((PI - t) / 2),(t / 2)) as Real ;
A45: ( s2 <= (PI - t) / 2 & s2 <= t / 2 ) by XXREAL_0:17;
then A47: t - (t / 2) <= t - s2 by XREAL_1:13;
A48: t + s2 <= t + ((PI - t) / 2) by A45, XREAL_1:7;
A42: 0 < PI - t by A38, XREAL_1:50;
then ( 0 < (PI - t) / 2 & (PI - t) / 2 < PI - t ) by XREAL_1:216;
then ((PI - t) / 2) + t < (PI - t) + t by XREAL_1:8;
then A49: t + s2 < PI by A48, XXREAL_0:2;

B49: now :: thesis:

let z be object ; :: thesis:
assume A50: z in ].(t - s2),(t + s2).[ ; :: thesis:
then reconsider s = z as Real ;
A51: ( t - s2 < s & s < t + s2 ) by A50, XXREAL_1:4;
then s < PI by A49, XXREAL_0:2;
hence z in ].0,PI.[ by A44, A47, A51; :: thesis:

end;

then A53: ( 0 < s2 & ].(t - s2),(t + s2).[ c= ].0,PI.[ ) by A38, A42, XXREAL_0:15;
reconsider s = min (s1,s2) as Real ;
A54: ( s <= s1 & s <= s2 ) by XXREAL_0:17;
take s = s; :: thesis:
thus 0 < s by A41, A53, XXREAL_0:15; :: thesis:
thus for t1 being Real st t1 in dom u & |.(t1 - t).| < s holds
|.((u . t1) - (u . t)).| < r :: thesis:

proof

end;

hence u is_continuous_in t by FCONT_1:3; :: thesis:

end;

suppose A60: t = PI ; :: thesis:

consider d being Real such that
A61: ( 0 < d & ].(t - d),(t + d).[ c= Z ) by A1, A23, A36, RCOMP_1:19;
A62: ( 0 < PI / 2 & PI / 2 < PI ) by LmPI, XREAL_1:216;
reconsider d0 = min (d,(PI / 2)) as Real ;
A63: ( d0 <= d & d0 <= PI / 2 ) by XXREAL_0:17;
A64: 0 < d0 by A61, LmPI, XXREAL_0:15;
reconsider N = ].(PI - d0),(PI + d0).[ as Neighbourhood of t by A60, A64, RCOMP_1:def 6;

A65: now :: thesis:

let s be object ; :: thesis:
assume B65: s in N ; :: thesis:
then A66: ex r being Real st
( s = r & PI - d0 < r & r < PI + d0 ) ;
reconsider r = s as Real by B65;
PI - d <= PI - d0 by A63, XREAL_1:13;
then A68: PI - d < r by A66, XXREAL_0:2;
PI + d0 <= PI + d by A63, XREAL_1:7;
then r < PI + d by A66, XXREAL_0:2;
hence s in ].(PI - d),(PI + d).[ by A68; :: thesis:
PI - (PI / 2) <= PI - d0 by A63, XREAL_1:13;
then A69: PI - (PI / 2) < r by A66, XXREAL_0:2;
PI + d0 <= PI + (PI / 2) by A63, XREAL_1:7;
then r < PI + (PI / 2) by A66, XXREAL_0:2;
hence s in ].(PI / 2),(PI + (PI / 2)).[ by A69; :: thesis:

end;

then N c= ].(PI - d),(PI + d).[ ;
then A73: N c= dom y by A1, A60, A61;
A72: N c= Z by A60, A61, A65;
A74: ( y is_differentiable_on N & sin is_differentiable_on N ) by A1, A73, Th8, FDIFF_1:26;

now :: thesis:

let s be object ; :: thesis:
assume A75: s in N \ {t} ; :: thesis:
then reconsider r = s as Real ;
A76: ( r in N & not r in {t} ) by A75, XBOOLE_0:def 5;
then A77: r <> t by TARSKI:def 1;
A78: PI + (PI / 2) < PI + PI by A62, XREAL_1:8;
r in ].(PI / 2),(PI + (PI / 2)).[ by A65, A76;
then ( PI / 2 < r & r < PI + (PI / 2) ) by XXREAL_1:4;
then ( ( 0 < r & r < PI ) or ( PI < r & r < PI + PI ) ) by A60, A77, A78, LmPI, XXREAL_0:1, XXREAL_0:2;
then ( r in ].0,PI.[ or r in ].PI,(2 * PI).[ ) ;
then A79: sin . r <> 0 by COMPTRIG:7, COMPTRIG:9;
A80: dom sin = REAL by FUNCT_2:def 1;
A81: r in REAL by XREAL_0:def 1;
not r in sin " {0}

proof

assume r in sin " {0} ; :: thesis:
then ( r in dom sin & sin . r in {0} ) by FUNCT_1:def 7;
hence contradiction by A79, TARSKI:def 1; :: thesis:

end;

then A82: r in (dom sin) \ (sin " {0}) by A80, A81, XBOOLE_0:def 5;
s in (dom y) /\ ((dom sin) \ (sin " {0})) by A73, A76, A82, XBOOLE_0:def 4;
hence s in dom (y / sin) by RFUNCT_1:def 1; :: thesis:

end;

then A83: N \ {t} c= dom (y / sin) ;
A84: ( sin is_differentiable_on N & sin `| N = cos | N ) by Th8;
y is_differentiable_on N by A1, A73, FDIFF_1:26;
then A85: dom (y `| N) = N by FDIFF_1:def 7;

now :: thesis:

let s be object ; :: thesis:
assume A86: s in N ; :: thesis:
then reconsider r = s as Real ;
A88: dom (sin `| N) = dom (cos | N) by Th8
.= REAL /\ N by RELAT_1:61, SIN_COS:24
.= N by XBOOLE_1:28 ;
not r in (sin `| N) " {0}

proof

assume r in (sin `| N) " {0} ; :: thesis:
then (cos | N) . r in {0} by A84, FUNCT_1:def 7;
then cos . r in {0} by A86, FUNCT_1:49;
hence contradiction by A65, A86, COMPTRIG:13; :: thesis:

end;

then r in (dom (sin `| N)) \ ((sin `| N) " {0}) by A86, A88, XBOOLE_0:def 5;
then s in (dom (y `| N)) /\ ((dom (sin `| N)) \ ((sin `| N) " {0})) by A85, A86, XBOOLE_0:def 4;
hence s in dom ((y `| N) / (sin `| N)) by RFUNCT_1:def 1; :: thesis:

end;

then A91: N c= dom ((y `| N) / (sin `| N)) ;
A96: cos | N is continuous ;
dom (cos | N) = REAL /\ N by RELAT_1:61, SIN_COS:24
.= N by XBOOLE_1:28 ;
then A97: sin `| N is_continuous_in t by A84, A96, RCOMP_1:16;
(y `| Z) | N is continuous by A1;
then y `| N is continuous by A1, A72, Th18, FDIFF_1:28;
then A100: y `| N is_continuous_in t by A85, RCOMP_1:16;
(sin `| N) . t = (cos | N) . t by Th8
.= - 1 by A60, FUNCT_1:49, RCOMP_1:16, SIN_COS:76 ;
then A101: (y `| N) / (sin `| N) is_continuous_in t by A85, A97, A100, FCONT_1:11, RCOMP_1:16;
A102: ( y / sin is_convergent_in t & lim ((y / sin),t) = (diff (y,t)) / (diff (sin,t)) ) by A1, A60, A74, A83, A91, A101, L_HOSPIT:10, SIN_COS:76;

now :: thesis:

let r be Real; :: thesis:
assume A104: 0 < r ; :: thesis:
then consider e1 being Real such that
A105: ( 0 < e1 & ( for t1 being Real st 0 < |.(t - t1).| & |.(t - t1).| < e1 & t1 in dom (y / sin) holds
|.(((y / sin) . t1) - ((diff (y,t)) / (diff (sin,t)))).| < r ) ) by A102, LIMFUNC3:28;
reconsider e = min (e1,(PI / 2)) as Real ;
A106: ( e <= e1 & e <= PI / 2 ) by XXREAL_0:17;
take e = e; :: thesis:
thus 0 < e by A105, LmPI, XXREAL_0:15; :: thesis:
thus for t1 being Real st t1 in dom u & |.(t1 - t).| < e holds
|.((u . t1) - (u . t)).| < r :: thesis:

proof

let t1 be Real; :: thesis:
assume A107: ( t1 in dom u & |.(t1 - t).| < e ) ; :: thesis:
u . t = - (diff (y,t)) by A24, A60;
then A109: (diff (y,t)) / (diff (sin,t)) = (- (u . t)) / (- 1) by A60, SIN_COS:68, SIN_COS:76
.= u . t ;
A111: ( 0 <= t1 & t1 <= PI ) by A3, A23, A107, XXREAL_1:1;

per cases ;

suppose t = t1 ; :: thesis:

hence |.((u . t1) - (u . t)).| < r by A104, COMPLEX1:44; :: thesis:

end;

suppose A112: t <> t1 ; :: thesis:

then A113: t - t1 <> 0 ;
A114: t1 < PI by A60, A111, A112, XXREAL_0:1;
|.(t - t1).| < e by A107, COMPLEX1:60;
then t - t1 < e by A60, A111, COMPLEX1:43, XREAL_1:48;
then (t - t1) + t1 < e + t1 by XREAL_1:8;
then A116: t - e < (e + t1) - e by XREAL_1:14;
t - (PI / 2) <= t - e by A106, XREAL_1:13;
then A117: t1 in ].0,PI.[ by A60, A62, A114, A116;
|.(t - t1).| < e by A107, COMPLEX1:60;
then |.(t - t1).| < e1 by A106, XXREAL_0:2;
then |.(((y / sin) . t1) - ((diff (y,t)) / (diff (sin,t)))).| < r by A21, A105, A113, A117, COMPLEX1:47;
hence |.((u . t1) - (u . t)).| < r by A23, A107, A109, A117; :: thesis:

end;

hence u is_continuous_in t by FCONT_1:3; :: thesis:

end;

suppose A120: t = 0 ; :: thesis:

consider d being Real such that
A121: ( 0 < d & ].(t - d),(t + d).[ c= Z ) by A1, A23, A36, RCOMP_1:19;
A122: ( 0 < PI / 2 & PI / 2 < PI ) by LmPI, XREAL_1:216;
reconsider d0 = min (d,(PI / 2)) as Real ;
A123: - PI < - (PI / 2) by LmPI, XREAL_1:24, XREAL_1:216;
A124: ( d0 <= d & d0 <= PI / 2 ) by XXREAL_0:17;
A125: 0 < d0 by A121, LmPI, XXREAL_0:15;
reconsider N = ].(0 - d0),(0 + d0).[ as Neighbourhood of t by A120, A125, RCOMP_1:def 6;

A126: now :: thesis:

let s be object ; :: thesis:
assume B126: s in N ; :: thesis:
then reconsider r = s as Real ;
A127: ( 0 - d0 < r & r < 0 + d0 ) by B126, XXREAL_1:4;
0 - d <= 0 - d0 by A124, XREAL_1:13;
then A129: 0 - d < r by A127, XXREAL_0:2;
r < 0 + d by A124, A127, XXREAL_0:2;
hence s in ].(- d),d.[ by A129; :: thesis:
0 - (PI / 2) <= 0 - d0 by A124, XREAL_1:13;
then A130: 0 - (PI / 2) < r by A127, XXREAL_0:2;
r < PI / 2 by A124, A127, XXREAL_0:2;
hence s in ].(- (PI / 2)),(PI / 2).[ by A130; :: thesis:

end;

then A131: N c= ].(0 - d),(0 + d).[ ;
A133: N c= Z by A120, A121, A126;
N c= dom y by A1, A120, A121, A131;
then A134: ( y is_differentiable_on N & sin is_differentiable_on N ) by A1, Th8, FDIFF_1:26;

now :: thesis:

let s be object ; :: thesis:
assume A135: s in N \ {t} ; :: thesis:
then reconsider r = s as Real ;
A136: ( r in N & not r in {t} ) by A135, XBOOLE_0:def 5;
then A137: r <> t by TARSKI:def 1;
r in ].(- (PI / 2)),(PI / 2).[ by A126, A136;
then ( - (PI / 2) < r & r < PI / 2 ) by XXREAL_1:4;
then ( ( - PI < r & r < 0 ) or ( 0 < r & r < PI ) ) by A120, A122, A123, A137, XXREAL_0:2;
then ( r in ].(- PI),0.[ or r in ].0,PI.[ ) ;
then A138: sin . r <> 0 by COMPTRIG:7, Lm13;
A139: dom sin = REAL by FUNCT_2:def 1;
A140: r in REAL by XREAL_0:def 1;
not r in sin " {0}

proof

assume r in sin " {0} ; :: thesis:
then ( r in dom sin & sin . r in {0} ) by FUNCT_1:def 7;
hence contradiction by A138, TARSKI:def 1; :: thesis:

end;

then A141: r in (dom sin) \ (sin " {0}) by A139, A140, XBOOLE_0:def 5;
r in dom y by A1, A133, A136;
then s in (dom y) /\ ((dom sin) \ (sin " {0})) by A141, XBOOLE_0:def 4;
hence s in dom (y / sin) by RFUNCT_1:def 1; :: thesis:

end;

then A142: N \ {t} c= dom (y / sin) ;
A143: ( sin is_differentiable_on N & sin `| N = cos | N ) by Th8;
A144: dom (y `| N) = N by A134, FDIFF_1:def 7;

now :: thesis:

let s be object ; :: thesis:
assume A145: s in N ; :: thesis:
then reconsider r = s as Real ;
A146: cos . r <> 0 by A126, A145, COMPTRIG:11;
A147: dom (sin `| N) = dom (cos | N) by Th8
.= REAL /\ N by RELAT_1:61, SIN_COS:24
.= N by XBOOLE_1:28 ;
not r in (sin `| N) " {0}

proof

assume r in (sin `| N) " {0} ; :: thesis:
then ( r in dom (sin `| N) & (sin `| N) . r in {0} ) by FUNCT_1:def 7;
then cos . r in {0} by A143, A145, FUNCT_1:49;
hence contradiction by A146, TARSKI:def 1; :: thesis:

end;

then r in (dom (sin `| N)) \ ((sin `| N) " {0}) by A145, A147, XBOOLE_0:def 5;
then s in (dom (y `| N)) /\ ((dom (sin `| N)) \ ((sin `| N) " {0})) by A144, A145, XBOOLE_0:def 4;
hence s in dom ((y `| N) / (sin `| N)) by RFUNCT_1:def 1; :: thesis:

end;

then A150: N c= dom ((y `| N) / (sin `| N)) ;
A155: cos | N is continuous ;
dom (cos | N) = N by RELAT_1:62, SIN_COS:24;
then A156: sin `| N is_continuous_in t by A143, A155, RCOMP_1:16;
y `| N = (y `| Z) | N by A1, A133, Th18, FDIFF_1:26;
then y `| N is continuous by A1;
then A157: y `| N is_continuous_in t by A144, RCOMP_1:16;
(sin `| N) . t = (cos | N) . t by Th8
.= 1 by A120, FUNCT_1:49, RCOMP_1:16, SIN_COS:30 ;
then A158: (y `| N) / (sin `| N) is_continuous_in t by A144, A156, A157, FCONT_1:11, RCOMP_1:16;
A159: ( y / sin is_convergent_in t & lim ((y / sin),t) = (diff (y,t)) / (diff (sin,t)) ) by A1, A120, A134, A142, A150, A158, L_HOSPIT:10, SIN_COS:30;

now :: thesis:

let r be Real; :: thesis:
assume A161: 0 < r ; :: thesis:
then consider e1 being Real such that
A162: ( 0 < e1 & ( for t1 being Real st 0 < |.(t - t1).| & |.(t - t1).| < e1 & t1 in dom (y / sin) holds
|.(((y / sin) . t1) - ((diff (y,t)) / (diff (sin,t)))).| < r ) ) by A159, LIMFUNC3:28;
reconsider e = min (e1,(PI / 2)) as Real ;
A163: ( e <= e1 & e <= PI / 2 ) by XXREAL_0:17;
take e = e; :: thesis:
thus 0 < e by A162, LmPI, XXREAL_0:15; :: thesis:
thus for t1 being Real st t1 in dom u & |.(t1 - t).| < e holds
|.((u . t1) - (u . t)).| < r :: thesis:

proof

let t1 be Real; :: thesis:
assume A164: ( t1 in dom u & |.(t1 - t).| < e ) ; :: thesis:
A165: (diff (y,t)) / (diff (sin,t)) = (diff (y,t)) / 1 by A120, SIN_COS:30, SIN_COS:68
.= u . t by A24, A120 ;
A167: ( 0 <= t1 & t1 <= PI ) by A3, A23, A164, XXREAL_1:1;

per cases ;

suppose t = t1 ; :: thesis:

hence |.((u . t1) - (u . t)).| < r by A161, COMPLEX1:44; :: thesis:

end;

suppose A168: t <> t1 ; :: thesis:

then A169: t - t1 <> 0 ;
t1 - t < e by A120, A164, A167, COMPLEX1:43;
then t1 < PI / 2 by A120, A163, XXREAL_0:2;
then t1 < PI by A122, XXREAL_0:2;
then A171: t1 in ].0,PI.[ by A120, A167, A168;
|.(t - t1).| < e by A164, COMPLEX1:60;
then |.(t - t1).| < e1 by A163, XXREAL_0:2;
then |.(((y / sin) . t1) - ((diff (y,t)) / (diff (sin,t)))).| < r by A21, A162, A169, A171, COMPLEX1:47;
hence |.((u . t1) - (u . t)).| < r by A23, A164, A165, A171; :: thesis:

end;

hence u is_continuous_in t by FCONT_1:3; :: thesis:

end;

then A174: u is continuous ;
for t being Real st t in ].0,PI.[ holds
u is_differentiable_in t

proof

let t be Real; :: thesis:
assume A175: t in ].0,PI.[ ; :: thesis:
then y / sin is_differentiable_in t by A11;
then u | ].0,PI.[ is_differentiable_in t by A21, A35, A175, Th14;
hence u is_differentiable_in t by A4, A23, A175, Th14; :: thesis:

end;

then A176: u is_differentiable_on ].0,PI.[ by A3, A23, Lm1, FDIFF_1:9;
B176: for t being Real st t in ].0,PI.[ holds
y / sin is_differentiable_in t by A11;
then A177: y / sin is_differentiable_on ].0,PI.[ by A21, FDIFF_1:9;
set DYS = (((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin);
A178: dom ((y / sin) `| ].0,PI.[) = ].0,PI.[ by A177, FDIFF_1:def 7;
A179: dom ((y `| Z) (#) sin) = (dom (y `| Z)) /\ (dom sin) by VALUED_1:def 4
.= Z /\ (dom sin) by A7, FDIFF_1:def 7
.= Z /\ REAL by FUNCT_2:def 1
.= Z by XBOOLE_1:28 ;
dom (cos (#) y) = (dom cos) /\ (dom y) by VALUED_1:def 4
.= REAL /\ (dom y) by FUNCT_2:def 1
.= dom y by XBOOLE_1:28 ;
then B179: dom (((y `| Z) (#) sin) - (cos (#) y)) = Z /\ (dom y) by A179, VALUED_1:12
.= Z by A1, XBOOLE_1:28 ;
then A180: ].0,PI.[ c= dom (((y `| Z) (#) sin) - (cos (#) y)) by A1, A4;

now :: thesis:

let t be object ; :: thesis:
assume A181: t in ].0,PI.[ ; :: thesis:
then reconsider s = t as Real ;
A182: dom (sin (#) sin) = REAL by FUNCT_2:def 1;
A183: s in REAL by XREAL_0:def 1;
A184: sin . s <> 0 by A181, COMPTRIG:7;
not s in (sin (#) sin) " {0}

proof

assume s in (sin (#) sin) " {0} ; :: thesis:
then ( s in dom (sin (#) sin) & (sin (#) sin) . s in {0} ) by FUNCT_1:def 7;
then (sin . s) * (sin . s) in {0} by VALUED_1:5;
hence contradiction by A184, TARSKI:def 1; :: thesis:

end;

hence t in (dom (sin (#) sin)) \ ((sin (#) sin) " {0}) by A182, A183, XBOOLE_0:def 5; :: thesis:

end;

then A185: ].0,PI.[ c= (dom (sin (#) sin)) \ ((sin (#) sin) " {0}) ;
then ].0,PI.[ /\ ].0,PI.[ c= (dom (((y `| Z) (#) sin) - (cos (#) y))) /\ ((dom (sin (#) sin)) \ ((sin (#) sin) " {0})) by A180, XBOOLE_1:27;
then A186: ].0,PI.[ c= dom ((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) by RFUNCT_1:def 1;
then A187: dom (((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) | ].0,PI.[) = ].0,PI.[ by RELAT_1:62;
for t being object st t in dom ((y / sin) `| ].0,PI.[) holds
((y / sin) `| ].0,PI.[) . t = (((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) | ].0,PI.[) . t

proof

let t be object ; :: thesis:
assume B187: t in dom ((y / sin) `| ].0,PI.[) ; :: thesis:
then A188: t in ].0,PI.[ by A177, FDIFF_1:def 7;
reconsider s = t as Real by B187;
A189: s in Z by A1, A4, A188;
thus ((y / sin) `| ].0,PI.[) . t = diff ((y / sin),s) by A177, A188, FDIFF_1:def 7
.= (((diff (y,s)) * (sin . s)) - ((diff (sin,s)) * (y . s))) / ((sin . s) ^2) by A11, A188
.= ((((y `| Z) . s) * (sin . s)) - ((diff (sin,s)) * (y . s))) / ((sin . s) ^2) by A7, A189, FDIFF_1:def 7
.= ((((y `| Z) . s) * (sin . s)) - ((cos . s) * (y . s))) / ((sin . s) ^2) by SIN_COS:64
.= ((((y `| Z) (#) sin) . s) - ((cos . s) * (y . s))) * (((sin . s) ^2) ") by VALUED_1:5
.= ((((y `| Z) (#) sin) . s) - ((cos (#) y) . s)) * (((sin . s) ^2) ") by VALUED_1:5
.= ((((y `| Z) (#) sin) - (cos (#) y)) . s) * (((sin . s) ^2) ") by A1, A4, B179, A188, VALUED_1:13
.= ((((y `| Z) (#) sin) - (cos (#) y)) . s) * (((sin (#) sin) . s) ") by VALUED_1:5
.= ((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) . s by A186, A188, RFUNCT_1:def 1
.= (((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) | ].0,PI.[) . t by A188, FUNCT_1:49 ; :: thesis:

end;

then A192: (y / sin) `| ].0,PI.[ = ((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) | ].0,PI.[ by A178, A187, FUNCT_1:2;
y | (dom y) is continuous by A1, FDIFF_1:25;
then A194: ((y `| Z) (#) sin) - (cos (#) y) is continuous by A1;
A195: dom (sin (#) sin) = REAL by FUNCT_2:def 1;
for t being Real st t in dom (((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) | ].0,PI.[) holds
((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) | ].0,PI.[ is_continuous_in t

proof

let t be Real; :: thesis:
assume A196: t in dom (((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) | ].0,PI.[) ; :: thesis:
then A197: not t in (sin (#) sin) " {0} by A185, A187, XBOOLE_0:def 5;
A198: (sin (#) sin) . t <> 0

proof

assume (sin (#) sin) . t = 0 ; :: thesis:
then (sin (#) sin) . t in {0} by TARSKI:def 1;
hence contradiction by A195, A196, A197, FUNCT_1:def 7; :: thesis:

end;

A201: ((y `| Z) (#) sin) - (cos (#) y) is_continuous_in t by A1, A4, B179, A187, A194, A196;
sin (#) sin is_continuous_in t by A195, A196, FCONT_1:def 2;
then (((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin) is_continuous_in t by A1, A4, B179, A187, A196, A198, A201, FCONT_1:11;
hence ((((y `| Z) (#) sin) - (cos (#) y)) / (sin (#) sin)) | ].0,PI.[ is_continuous_in t by A187, A196, FCONT_1:1; :: thesis:

end;

then A202: (y / sin) `| ].0,PI.[ is continuous by A192;
B202: u `| ].0,PI.[ = (u | ].0,PI.[) `| ].0,PI.[ by A176, Th17
.= ((y / sin) | ].0,PI.[) `| ].0,PI.[ by A31, A32, B32, FUNCT_1:2
.= (y / sin) `| ].0,PI.[ by A21, Th17, B176, FDIFF_1:9 ;
A204: ( sin is_differentiable_on ].0,PI.[ & sin `| ].0,PI.[ = cos | ].0,PI.[ & cos is_differentiable_on ].0,PI.[ & cos `| ].0,PI.[ = - (sin | ].0,PI.[) ) by Th8;
A205: dom (y | ['0,PI']) = (dom y) /\ ['0,PI'] by RELAT_1:61
.= ['0,PI'] by A9, XBOOLE_1:28 ;
A207: dom (u (#) sin) = (dom u) /\ (dom sin) by VALUED_1:def 4
.= ['0,PI'] /\ REAL by A23, FUNCT_2:def 1
.= ['0,PI'] by XBOOLE_1:28 ;
B207: for t being object st t in dom (y | ['0,PI']) holds
(y | ['0,PI']) . t = (u (#) sin) . t

proof

let t be object ; :: thesis:
assume A208: t in dom (y | ['0,PI']) ; :: thesis:
then reconsider s = t as Real ;
ex r being Real st
( r = s & 0 <= r & r <= PI ) by A3, A205, A208;

per cases by XXREAL_0:1;

suppose 0 = s ; :: thesis:

hence (y | ['0,PI']) . t = (u . s) * (sin . s) by A1, A205, A208, FUNCT_1:49, SIN_COS:30
.= (u (#) sin) . t by VALUED_1:5 ;
:: thesis:

end;

suppose ( 0 < s & s < PI ) ; :: thesis:

then A211: s in ].0,PI.[ ;
then A212: sin s <> 0 by COMPTRIG:7;
(u (#) sin) . t = (u . s) * (sin . s) by VALUED_1:5
.= ((u | ].0,PI.[) . s) * (sin . s) by A211, FUNCT_1:49
.= (((y / sin) | ].0,PI.[) . s) * (sin . s) by A31, A32, B32, FUNCT_1:2
.= ((y / sin) . s) * (sin . s) by A211, FUNCT_1:49
.= ((y . s) * ((sin . s) ")) * (sin . s) by B15, A211, RFUNCT_1:def 1
.= ((y . s) * (sin . s)) * ((sin . s) ")
.= y . t by A212, XCMPLX_1:203 ;
hence (y | ['0,PI']) . t = (u (#) sin) . t by A205, A208, FUNCT_1:49; :: thesis:

end;

suppose s = PI ; :: thesis:

hence (y | ['0,PI']) . t = (u . s) * (sin . s) by A1, A205, A208, FUNCT_1:49, SIN_COS:76
.= (u (#) sin) . t by VALUED_1:5 ;
:: thesis:

end;

then A216: y | ['0,PI'] = (u (#) sin) | ['0,PI'] by A205, A207, FUNCT_1:2;
A217: y | ].0,PI.[ = (y | ['0,PI']) | ].0,PI.[ by A3, Lm1, RELAT_1:74
.= (u (#) sin) | ].0,PI.[ by A205, A207, B207, FUNCT_1:2 ;
B217: y | ].0,PI.[ is_differentiable_on ].0,PI.[ by A10, Th16;
then A218: u (#) sin is_differentiable_on ].0,PI.[ by A217, Th16;
for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t))

proof

let t be Real; :: thesis:
assume A220: t in ].0,PI.[ ; :: thesis:
then A222: ((u (#) sin) `| ].0,PI.[) . t = ((sin . t) * (diff (u,t))) + ((u . t) * (diff (sin,t))) by A176, A204, A218, FDIFF_1:21
.= ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) by SIN_COS:64 ;
diff (y,t) = (y `| ].0,PI.[) . t by A10, A220, FDIFF_1:def 7
.= (((u (#) sin) | ].0,PI.[) `| ].0,PI.[) . t by A5, A7, A217, Th17, FDIFF_1:26
.= ((u (#) sin) `| ].0,PI.[) . t by A217, B217, Th16, Th17 ;
hence diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) by A222; :: thesis:

end;

hence ex u being PartFunc of REAL,REAL st
( 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 A23, A174, A176, A202, B202, A216; :: thesis: