reconsider S = <:T,T9:> as Function of the carrier' of C, the carrier' of [:D,D9:] ;

now :: thesis: ( ( 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 :: thesis: ( ( 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) ) )

proof

let c be Object of C; :: thesis: ex dd9 being Object of [:D,D9:] st S . (id c) = id dd9
set d = (Obj T) . c;
set d9 = (Obj T9) . c;
take dd9 = [((Obj T) . c),((Obj T9) . c)]; :: thesis: S . (id c) = id dd9
thus S . (id c) = [(T . (id c)),(T9 . (id c))] by FUNCT_3:59
.= [(id ((Obj T) . c)),(T9 . (id c))] by CAT_1:68
.= [(id ((Obj T) . c)),(id ((Obj T9) . c))] by CAT_1:68
.= id dd9 by Th25 ; :: thesis: verum

end;

thus for f being Morphism of C holds
( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) ) :: thesis: for f, g being Morphism of C st dom g = cod f holds
S . (g (*) f) = (S . g) (*) (S . f)

proof

let f be Morphism of C; :: thesis: ( S . (id (dom f)) = id (dom (S . f)) & S . (id (cod f)) = id (cod (S . f)) )
( T . (id (dom f)) = id (dom (T . f)) & T9 . (id (dom f)) = id (dom (T9 . f)) ) by CAT_1:63;
hence S . (id (dom f)) = [(id (dom (T . f))),(id (dom (T9 . f)))] by FUNCT_3:59
.= id [(dom (T . f)),(dom (T9 . f))] by Th25
.= id (dom [(T . f),(T9 . f)]) by Th22
.= id (dom (S . f)) by FUNCT_3:59 ;
:: thesis: S . (id (cod f)) = id (cod (S . f))
( T . (id (cod f)) = id (cod (T . f)) & T9 . (id (cod f)) = id (cod (T9 . f)) ) by CAT_1:63;
hence S . (id (cod f)) = [(id (cod (T . f))),(id (cod (T9 . f)))] by FUNCT_3:59
.= id [(cod (T . f)),(cod (T9 . f))] by Th25
.= id (cod [(T . f),(T9 . f)]) by Th22
.= id (cod (S . f)) by FUNCT_3:59 ;
:: thesis: verum

end;

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies S . (g (*) f) = (S . g) (*) (S . f) )
assume A1: dom g = cod f ; :: thesis: 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 ;
:: thesis: verum

end;

hence <:T,T9:> is Functor of C,[:D,D9:] by CAT_1:61; :: thesis: verum