reconsider S = <:T,T9:> as Function of the carrier' of C, the carrier' of [:D,D9:] ;
now ( ( for c being Object of C ex dd9 being Object of [:D,D9:] st S . (id c) = id dd9 ) & ( for f being Morphism of C holds
( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
S . (g (*) f) = (S . g) (*) (S . f) ) )thus
for
c being
Object of
C ex
dd9 being
Object of
[:D,D9:] st
S . (id c) = id dd9
( ( for f being Morphism of C holds
( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
S . (g (*) f) = (S . g) (*) (S . f) ) )thus
for
f being
Morphism of
C holds
(
S . (id (dom f)) = id (dom (S . f)) &
S . (id (cod f)) = id (cod (S . f)) )
for f, g being Morphism of C st dom g = cod f holds
S . (g (*) f) = (S . g) (*) (S . f)let f,
g be
Morphism of
C;
( dom g = cod f implies S . (g (*) f) = (S . g) (*) (S . f) )assume A1:
dom g = cod f
;
S . (g (*) f) = (S . g) (*) (S . f)then A2:
(
dom (T . g) = cod (T . f) &
dom (T9 . g) = cod (T9 . f) )
by CAT_1:64;
(
T . (g (*) f) = (T . g) (*) (T . f) &
T9 . (g (*) f) = (T9 . g) (*) (T9 . f) )
by A1, CAT_1:64;
hence S . (g (*) f) =
[((T . g) (*) (T . f)),((T9 . g) (*) (T9 . f))]
by FUNCT_3:59
.=
[(T . g),(T9 . g)] (*) [(T . f),(T9 . f)]
by A2, Th23
.=
(S . g) (*) [(T . f),(T9 . f)]
by FUNCT_3:59
.=
(S . g) (*) (S . f)
by FUNCT_3:59
;
verum end;
hence
<:T,T9:> is Functor of C,[:D,D9:]
by CAT_1:61; verum