let
x
be
Element
of
Funct
(
C
,
D
);
:: according to
CAT_2:def 3
:: thesis:
x
is
Functor
of
C
,
D
thus
x
is
Functor
of
C
,
D
by
Def2
;
:: thesis:
verum