let C, D, D' be Category; :: thesis: for T being Functor of C,D
for T' being Functor of C,D' holds <:T,T':> is Functor of C,[:D,D':]
let T be Functor of C,D; :: thesis: for T' being Functor of C,D' holds <:T,T':> is Functor of C,[:D,D':]
let T' be Functor of C,D'; :: thesis: <:T,T':> is Functor of C,[:D,D':]
reconsider S = <:T,T':> as Function of the carrier' of C,the carrier' of [:D,D':] ;

now

thus for c being Object of C ex dd' being Object of [:D,D':] st S . (id c) = id dd' :: 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 dd' being Object of [:D,D':] st S . (id c) = id dd'
set d = (Obj T) . c;
set d' = (Obj T') . c;
take dd' = [((Obj T) . c),((Obj T') . c)]; :: thesis: S . (id c) = id dd'
thus S . (id c) = [(T . (id c)),(T' . (id c))] by FUNCT_3:79
.= [(id ((Obj T) . c)),(T' . (id c))] by CAT_1:104
.= [(id ((Obj T) . c)),(id ((Obj T') . c))] by CAT_1:104
.= id dd' by Th41 ; :: 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)) & T' . (id (dom f)) = id (dom (T' . f)) ) by CAT_1:98;
hence S . (id (dom f)) = [(id (dom (T . f))),(id (dom (T' . f)))] by FUNCT_3:79
.= id [(dom (T . f)),(dom (T' . f))] by Th41
.= id (dom [(T . f),(T' . f)]) by Th38
.= id (dom (S . f)) by FUNCT_3:79 ;
:: thesis: S . (id (cod f)) = id (cod (S . f))
( T . (id (cod f)) = id (cod (T . f)) & T' . (id (cod f)) = id (cod (T' . f)) ) by CAT_1:98;
hence S . (id (cod f)) = [(id (cod (T . f))),(id (cod (T' . f)))] by FUNCT_3:79
.= id [(cod (T . f)),(cod (T' . f))] by Th41
.= id (cod [(T . f),(T' . f)]) by Th38
.= id (cod (S . f)) by FUNCT_3:79 ;
:: 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 (T' . g) = cod (T' . f) ) by CAT_1:99;
( T . (g * f) = (T . g) * (T . f) & T' . (g * f) = (T' . g) * (T' . f) ) by A1, CAT_1:99;
hence S . (g * f) = [((T . g) * (T . f)),((T' . g) * (T' . f))] by FUNCT_3:79
.= [(T . g),(T' . g)] * [(T . f),(T' . f)] by A2, Th39
.= (S . g) * [(T . f),(T' . f)] by FUNCT_3:79
.= (S . g) * (S . f) by FUNCT_3:79 ;
:: thesis: verum

end;

hence <:T,T':> is Functor of C,[:D,D':] by CAT_1:96; :: thesis: verum