let B, C, D be Category; :: thesis: for T being Functor of B,C
for S being Functor of C,D st T is faithful & S is faithful holds
S * T is faithful
let T be Functor of B,C; :: thesis: for S being Functor of C,D st T is faithful & S is faithful holds
S * T is faithful
let S be Functor of C,D; :: thesis: ( T is faithful & S is faithful implies S * T is faithful )
assume that
A1: T is faithful and
A2: S is faithful ; :: thesis: S * T is faithful
let b, b' be Object of B; :: according to CAT_1:def 24 :: thesis: ( Hom b,b' <> {} implies for f1, f2 being Morphism of b,b' st (S * T) . f1 = (S * T) . f2 holds
f1 = f2 )
assume A3: Hom b,b' <> {} ; :: thesis: for f1, f2 being Morphism of b,b' st (S * T) . f1 = (S * T) . f2 holds
f1 = f2
let f1, f2 be Morphism of b,b'; :: thesis: ( (S * T) . f1 = (S * T) . f2 implies f1 = f2 )
assume A4: (S * T) . f1 = (S * T) . f2 ; :: thesis: f1 = f2
( Hom (T . b),(T . b') <> {} & (S * T) . f1 = S . (T . f1) & (S * T) . f2 = S . (T . f2) & T . f1 is Morphism of T . b,T . b' & T . f2 is Morphism of T . b,T . b' ) by A3, Th125, Th126, FUNCT_2:21;
then T . f1 = T . f2 by A2, A4, Def24;
hence f1 = f2 by A1, A3, Def24; :: thesis: verum