(
dom
(
Shift
(
f
,
h
)
)
=
(

h
)
++
(
dom
f
)
&
dom
f
=
REAL
)
by
Def1
,
FUNCT_2:def 1
;
then
dom
(
Shift
(
f
,
h
)
)
=
REAL
by
MEASURE6:24
;
hence
Shift
(
f
,
h
) is
Function
of
REAL
,
REAL
by
FUNCT_2:def 1
;
:: thesis:
verum