let x be Real; :: thesis:

per cases ;

suppose A1: x > 0 ; :: thesis:

set X = [.0,(0 + x).];
reconsider X = [.0,(0 + x).] as set ;
AA: sin | X is continuous PartFunc of REAL,REAL ;
A4: sin is_differentiable_on ].0,(0 + x).[ by FDIFF_1:26, SIN_COS:68;
[.0,(0 + x).] c= REAL ;
then [.0,(0 + x).] c= dom sin by FUNCT_2:def 1;
then consider s being Real such that
0 < s and
s < 1 and
A2: sin . (0 + x) = (sin . 0) + (x * (diff (sin,(0 + (s * x))))) by A1, ROLLE:4, AA, A4;
|.(cos (s * x)).| <= 1 by SIN_COS:27;
then ( |.(cos . (s * x)).| <= 1 & 0 <= |.x.| ) by COMPLEX1:46, SIN_COS:def 19;
then A6: |.x.| * |.(cos . (s * x)).| <= |.x.| * 1 by XREAL_1:64;
|.(sin x).| = |.(sin . x).| by SIN_COS:def 17
.= |.(x * (cos . (s * x))).| by SIN_COS:64, SIN_COS:30, A2
.= |.x.| * |.(cos . (s * x)).| by COMPLEX1:65 ;
hence |.(sin x).| <= |.x.| by A6; :: thesis:

end;

suppose B1a: x < 0 ; :: thesis:

set X1 = [.0,(0 + (- x)).];
reconsider X1 = [.0,(0 + (- x)).] as set ;
B3a: sin | X1 is continuous PartFunc of REAL,REAL ;
B4: sin is_differentiable_on ].0,(0 + (- x)).[ by FDIFF_1:26, SIN_COS:68;
[.0,(0 + (- x)).] c= REAL ;
then [.0,(0 + (- x)).] c= dom sin by FUNCT_2:def 1;
then consider s being Real such that
0 < s and
s < 1 and
B2: sin . (0 + (- x)) = (sin . 0) + ((- x) * (diff (sin,(0 + (s * (- x)))))) by B1a, ROLLE:4, B3a, B4;
|.(cos (s * (- x))).| <= 1 by SIN_COS:27;
then ( |.(cos . (s * (- x))).| <= 1 & 0 <= |.(- x).| ) by COMPLEX1:46, SIN_COS:def 19;
then BB: |.(- x).| * |.(cos . (s * (- x))).| <= |.(- x).| * 1 by XREAL_1:64;
|.(sin x).| = |.(sin . x).| by SIN_COS:def 17
.= |.(- (sin . x)).| by COMPLEX1:52
.= |.(0 + ((- x) * (diff (sin,(0 + (s * (- x))))))).| by SIN_COS:30, B2
.= |.((- x) * (cos . (s * (- x)))).| by SIN_COS:64
.= |.(- x).| * |.(cos . (s * (- x))).| by COMPLEX1:65 ;
hence |.(sin x).| <= |.x.| by BB, COMPLEX1:52; :: thesis:

end;

suppose Z1: x = 0 ; :: thesis:

then |.(sin x).| = |.0.| by SIN_COS:31;
hence |.(sin x).| <= |.x.| by Z1; :: thesis:

end;

end;