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