let
i
be
object
;
:: according to
FUNCOP_1:def 6
:: thesis:
(
i
in
dom
(
f

C
)
implies
(
f

C
)
.
i
is
Function
)
f
.
i
is
Function
;
hence
(
i
in
dom
(
f

C
)
implies
(
f

C
)
.
i
is
Function
)
by
FUNCT_1:47
;
:: thesis:
verum