let B, C, D be Category; :: thesis: for T being Functor of B,C
for S being Functor of C,D
for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
let T be Functor of B,C; :: thesis: for S being Functor of C,D
for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
let S be Functor of C,D; :: thesis: for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
let b be Object of B; :: thesis: (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
A1: (S * T) . (id b) = S . (T . (id b)) by FUNCT_2:15;
consider d being Object of D such that
A2: (S * T) . (id b) = id d by Def19;
consider c being Object of C such that
A3: T . (id b) = id c by Def19;
thus (Obj (S * T)) . b = d by A2, Th62
.= (Obj S) . c by A2, A3, A1, Th62
.= (Obj S) . ((Obj T) . b) by A3, Th62 ; :: thesis: verum