let x be real number ; :: thesis: ( sin . x in [.(- 1),1.] & cos . x in [.(- 1),1.] )
( abs (sin x) <= 1 & abs (cos x) <= 1 ) by SIN_COS:30;
then ( abs (sin . x) <= 1 & abs (cos . x) <= 1 ) by SIN_COS:def 21, SIN_COS:def 23;
then ( - 1 <= sin . x & sin . x <= 1 & - 1 <= cos . x & cos . x <= 1 ) by ABSVALUE:12;
hence ( sin . x in [.(- 1),1.] & cos . x in [.(- 1),1.] ) by XXREAL_1:1; :: thesis: verum