A1
:
sin
=
R^1
sin
;
R^1

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