let x be Real; :: thesis: ( sin . x in [.(- 1),1.] & cos . x in [.(- 1),1.] )
|.(cos x).| <= 1 by SIN_COS:27;
then |.(cos . x).| <= 1 by SIN_COS:def 19;
then A1: ( - 1 <= cos . x & cos . x <= 1 ) by ABSVALUE:5;
|.(sin x).| <= 1 by SIN_COS:27;
then |.(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