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