let x, y be PartFunc of REAL,REAL; :: thesis:
let Z be open Subset of REAL; :: thesis:
assume that
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 ) and
A2: ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) ; :: thesis:
set X = ].0,PI.[;
A4: ['0,PI'] = [.0,PI.] by INTEGRA5:def 3, LEIBNIZ1:17;
then A5: ].0,PI.[ c= ['0,PI'] by Lm1;
A6: ].0,PI.[ c= Z by A1, A5;
A7: x is_differentiable_on Z by A1, FDIFF_1:26;
then A8: dom (x `| Z) = Z by FDIFF_1:def 7;
y is_differentiable_on dom y by A1;
then A9: y is continuous by FDIFF_1:25;
A10: dom (y (#) (x `| Z)) = (dom y) /\ Z by A8, VALUED_1:def 4
.= Z by A1, XBOOLE_1:28 ;
A11: REAL c= REAL ;

now :: thesis:

let r be Element of REAL ; :: thesis:
assume r in REAL ; :: thesis:
].(r - 1),(r + 1).[ is Neighbourhood of r by RCOMP_1:def 6;
hence ex N being Neighbourhood of r st N c= REAL ; :: thesis:

end;

then A13: REAL is open Subset of REAL by A11, RCOMP_1:20;
A14: ( cos is_differentiable_on REAL & cos `| REAL = - (sin | REAL) ) by A13, Th8;
A15: ( sin is_differentiable_on REAL & sin `| REAL = cos | REAL ) by A13, Th8;
A16: dom sin = REAL by FUNCT_2:def 1;
A17: dom cos = REAL by FUNCT_2:def 1;
A18: dom (sin (#) sin) = REAL by FUNCT_2:def 1;
A19: for t being Real st t in ].0,PI.[ holds
(y (#) (x `| Z)) . t = (sin (#) sin) . t

proof

let s be Real; :: thesis:
assume A20: s in ].0,PI.[ ; :: thesis:

per cases by A2;

suppose A21: for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) ; :: thesis:

A22: y . s = sin . s by A4, A5, A20, A21;
A23: ( cos is_differentiable_in s & diff (cos,s) = - (sin . s) ) by SIN_COS:63;
then A24: ( (- 1) (#) cos is_differentiable_in s & diff (((- 1) (#) cos),s) = (- 1) * (diff (cos,s)) ) by FDIFF_1:15;
consider N being Neighbourhood of s such that
A26: ( N c= dom ((- 1) (#) cos) & ex L being LinearFunc ex R being RestFunc st
( diff (((- 1) (#) cos),s) = L . 1 & ( for p being Real st p in N holds
(((- 1) (#) cos) . p) - (((- 1) (#) cos) . s) = (L . (p - s)) + (R . (p - s)) ) ) ) by A24, FDIFF_1:def 5;
consider L being LinearFunc, R being RestFunc such that
A27: ( diff (((- 1) (#) cos),s) = L . 1 & ( for p being Real st p in N holds
(((- 1) (#) cos) . p) - (((- 1) (#) cos) . s) = (L . (p - s)) + (R . (p - s)) ) ) by A26;
consider N2 being Neighbourhood of s such that
A28: N2 c= ].0,PI.[ by A20, RCOMP_1:18;
consider Ns being Neighbourhood of s such that
A29: ( Ns c= N & Ns c= N2 ) by RCOMP_1:17;
A30: ].0,PI.[ c= [.0,PI.] by Lm1;
Ns c= ].0,PI.[ by A28, A29;
then A31: Ns c= dom x by A1, A6;
A32: for p being Real st p in Ns holds
(x . p) - (x . s) = (L . (p - s)) + (R . (p - s))

proof

let p be Real; :: thesis:
assume A33: p in Ns ; :: thesis:
then p in [.0,PI.] by A28, A29, A30;
hence (x . p) - (x . s) = (((- (cos . p)) + (cos . 0)) + (x . 0)) - (x . s) by A21
.= (((- (cos . p)) + (cos . 0)) + (x . 0)) - (((- (cos . s)) + (cos . 0)) + (x . 0)) by A20, A21, A30
.= (- (cos . p)) + (cos . s)
.= ((- cos) . p) - (- (cos . s)) by VALUED_1:8
.= ((- cos) . p) - ((- cos) . s) by VALUED_1:8
.= (L . (p - s)) + (R . (p - s)) by A27, A29, A33 ;
:: thesis:

end;

then x is_differentiable_in s by A31;
then A39: diff (x,s) = sin . s by A23, A24, A27, A31, A32, FDIFF_1:def 5;
thus (y (#) (x `| Z)) . s = (y . s) * ((x `| Z) . s) by VALUED_1:5
.= (y . s) * (diff (x,s)) by A6, A7, A20, FDIFF_1:def 7
.= (sin (#) sin) . s by A22, A39, VALUED_1:5 ; :: thesis:

end;

suppose A40: for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ; :: thesis:

then A41: y . s = - (sin . s) by A4, A5, A20;
A42: ( cos is_differentiable_in s & diff (cos,s) = - (sin . s) ) by SIN_COS:63;
consider N being Neighbourhood of s such that
A43: ( N c= dom cos & ex L being LinearFunc ex R being RestFunc st
( diff (cos,s) = L . 1 & ( for p being Real st p in N holds
(cos . p) - (cos . s) = (L . (p - s)) + (R . (p - s)) ) ) ) by A42, FDIFF_1:def 5;
consider L being LinearFunc, R being RestFunc such that
A44: ( diff (cos,s) = L . 1 & ( for p being Real st p in N holds
(cos . p) - (cos . s) = (L . (p - s)) + (R . (p - s)) ) ) by A43;
consider N2 being Neighbourhood of s such that
A45: N2 c= ].0,PI.[ by A20, RCOMP_1:18;
consider Ns being Neighbourhood of s such that
A46: ( Ns c= N & Ns c= N2 ) by RCOMP_1:17;
A47: ].0,PI.[ c= [.0,PI.] by Lm1;
Ns c= ].0,PI.[ by A45, A46;
then A48: Ns c= dom x by A1, A6;
A49: for p being Real st p in Ns holds
(x . p) - (x . s) = (L . (p - s)) + (R . (p - s))

proof

let p be Real; :: thesis:
assume A50: p in Ns ; :: thesis:
then p in [.0,PI.] by A45, A46, A47;
hence (x . p) - (x . s) = (((cos . p) - (cos . 0)) + (x . 0)) - (x . s) by A40
.= (((cos . p) - (cos . 0)) + (x . 0)) - (((cos . s) - (cos . 0)) + (x . 0)) by A20, A40, A47
.= (cos . p) - (cos . s)
.= (L . (p - s)) + (R . (p - s)) by A44, A46, A50 ;
:: thesis:

end;

then x is_differentiable_in s by A48;
then A56: diff (x,s) = - (sin . s) by A42, A44, A48, A49, FDIFF_1:def 5;
thus (y (#) (x `| Z)) . s = (y . s) * ((x `| Z) . s) by VALUED_1:5
.= (y . s) * (diff (x,s)) by A6, A7, A20, FDIFF_1:def 7
.= (sin . s) * (sin . s) by A41, A56
.= (sin (#) sin) . s by VALUED_1:5 ; :: thesis:

end;

(sin (#) sin) | ['0,PI'] is continuous ;
then A60: ( sin (#) sin is_integrable_on ['0,PI'] & (sin (#) sin) | ['0,PI'] is bounded ) by A18, INTEGRA5:10, INTEGRA5:11;
dom ((- 1) (#) cos) = REAL by FUNCT_2:def 1;
then A61: ( (- 1) (#) cos is_differentiable_on REAL & ((- 1) (#) cos) `| REAL = (- 1) (#) (cos `| REAL) ) by A13, A14, Th12;
then A62: ((- 1) (#) cos) `| REAL = ((- 1) * (- 1)) (#) (sin | REAL) by A14, RFUNCT_1:17
.= sin by RFUNCT_1:21 ;
set F = sin (#) ((- 1) (#) cos);
B62: dom (sin (#) ((- 1) (#) cos)) = (dom sin) /\ (dom ((- 1) (#) cos)) by VALUED_1:def 4
.= (dom sin) /\ (dom cos) by VALUED_1:def 5
.= REAL by A16, A17 ;
then A63: ( sin (#) ((- 1) (#) cos) is_differentiable_on REAL & (sin (#) ((- 1) (#) cos)) `| REAL = ((sin `| REAL) (#) ((- 1) (#) cos)) + (sin (#) (((- 1) (#) cos) `| REAL)) ) by A13, A15, A61, Th13;
set I = REAL --> 1;
A65: dom (REAL --> 1) = REAL by FUNCOP_1:13;
A66: rng (REAL --> 1) = {1} by FUNCOP_1:8;
rng (REAL --> 1) c= REAL ;
then reconsider I = REAL --> 1 as PartFunc of REAL,REAL by A65, RELSET_1:4;
A67: I is continuous by A66, FCONT_1:39;
then I | ['0,PI'] is continuous ;
then A71: ( I is_integrable_on ['0,PI'] & I | ['0,PI'] is bounded ) by A65, INTEGRA5:10, INTEGRA5:11;
A72: dom (((- 1) (#) cos) (#) cos) = (dom ((- 1) (#) cos)) /\ (dom cos) by VALUED_1:def 4
.= (dom cos) /\ (dom cos) by VALUED_1:def 5
.= REAL by FUNCT_2:def 1 ;
A73: dom ((sin (#) sin) - I) = (dom (sin (#) sin)) /\ (dom I) by VALUED_1:12
.= ((dom sin) /\ (dom sin)) /\ (dom I) by VALUED_1:def 4
.= REAL by A16, FUNCOP_1:13 ;

now :: thesis:

let t be object ; :: thesis:
assume A74: t in dom (((- 1) (#) cos) (#) cos) ; :: thesis:
then reconsider s = t as Real ;
A75: ((cos . s) * (cos . s)) + ((sin . s) * (sin . s)) = 1 by SIN_COS:28;
thus (((- 1) (#) cos) (#) cos) . t = (((- 1) (#) cos) . t) * (cos . t) by VALUED_1:5
.= ((- 1) * (cos . t)) * (cos . t) by VALUED_1:6
.= - ((cos . s) * (cos . s))
.= ((sin . s) * (sin . s)) - 1 by A75
.= ((sin . s) * (sin . s)) - (I . s) by FUNCOP_1:7, XREAL_0:def 1
.= ((sin (#) sin) . s) - (I . s) by VALUED_1:5
.= ((sin (#) sin) - I) . t by A73, A74, VALUED_1:13 ; :: thesis:

end;