let B, C, D be Category; :: thesis: for T being Functor of B,C
for S being Functor of C,D holds S * T is Functor of B,D
let T be Functor of B,C; :: thesis: for S being Functor of C,D holds S * T is Functor of B,D
let S be Functor of C,D; :: thesis: S * T is Functor of B,D
reconsider FF = (Obj S) * (Obj T) as Function of the carrier of B, the carrier of D ;
reconsider TT = S * T as Function of the carrier' of B, the carrier' of D ;

now :: thesis: ( ( for b being Object of B holds TT . (id b) = id (FF . b) ) & ( for f being Morphism of B holds
( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) ) ) & ( for f, g being Morphism of B st dom g = cod f holds
TT . (g (*) f) = (TT . g) (*) (TT . f) ) )

thus for b being Object of B holds TT . (id b) = id (FF . b) :: thesis: ( ( for f being Morphism of B holds
( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) ) ) & ( for f, g being Morphism of B st dom g = cod f holds
TT . (g (*) f) = (TT . g) (*) (TT . f) ) )

proof

let b be Object of B; :: thesis: TT . (id b) = id (FF . b)
thus TT . (id b) = S . (T . (id b)) by FUNCT_2:15
.= S . (id (T . b)) by Th63
.= id (S . ((Obj T) . b)) by Th63
.= id (FF . b) by FUNCT_2:15 ; :: thesis: verum

end;

thus for f being Morphism of B holds
( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) ) :: thesis: for f, g being Morphism of B st dom g = cod f holds
TT . (g (*) f) = (TT . g) (*) (TT . f)

proof

let f be Morphism of B; :: thesis: ( FF . (dom f) = dom (TT . f) & FF . (cod f) = cod (TT . f) )
thus FF . (dom f) = (Obj S) . ((Obj T) . (dom f)) by FUNCT_2:15
.= (Obj S) . (dom (T . f)) by Th64
.= dom (S . (T . f)) by Th64
.= dom (TT . f) by FUNCT_2:15 ; :: thesis: FF . (cod f) = cod (TT . f)
thus FF . (cod f) = (Obj S) . ((Obj T) . (cod f)) by FUNCT_2:15
.= (Obj S) . (cod (T . f)) by Th64
.= cod (S . (T . f)) by Th64
.= cod (TT . f) by FUNCT_2:15 ; :: thesis: verum

end;

let f, g be Morphism of B; :: thesis: ( dom g = cod f implies TT . (g (*) f) = (TT . g) (*) (TT . f) )
assume A1: dom g = cod f ; :: thesis: TT . (g (*) f) = (TT . g) (*) (TT . f)
then A2: dom (T . g) = cod (T . f) by Th59;
thus TT . (g (*) f) = S . (T . (g (*) f)) by FUNCT_2:15
.= S . ((T . g) (*) (T . f)) by A1, Th59
.= (S . (T . g)) (*) (S . (T . f)) by A2, Th59
.= (TT . g) (*) (S . (T . f)) by FUNCT_2:15
.= (TT . g) (*) (TT . f) by FUNCT_2:15 ; :: thesis: verum

end;

hence S * T is Functor of B,D by Th60; :: thesis: verum