A1
:
cos
=
R^1
cos
;
R^1

(
R^1
(
dom
cos
)
)
=
R^1
by
Th6
,
SIN_COS:24
;
hence
cos
is
Function
of
R^1
,
R^1
by
A1
,
COMPTRIG:29
,
TOPREALA:7
;
:: thesis:
verum