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

h
)
++
(
dom
f
)
&
dom
f
=
the
carrier
of
V
)
by
Def1
,
FUNCT_2:def 1
;
then
dom
(
Shift
(
f
,
h
)
)
=
the
carrier
of
V
by
MEASURE624
;
hence
Shift
(
f
,
h
) is
Function
of
V
,
W
by
FUNCT_2:def 1
;
:: thesis:
verum