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, b9 be Object of B; :: according to CAT_1:def 21 :: thesis: ( Hom (b,b9) <> {} implies for f1, f2 being Morphism of b,b9 st (S * T) . f1 = (S * T) . f2 holds
f1 = f2 )
assume A3: Hom (b,b9) <> {} ; :: thesis: for f1, f2 being Morphism of b,b9 st (S * T) . f1 = (S * T) . f2 holds
f1 = f2
let f1, f2 be Morphism of b,b9; :: thesis: ( (S * T) . f1 = (S * T) . f2 implies f1 = f2 )
A4: T . f2 is Morphism of T . b,T . b9 by A3, Th125;
assume A5: (S * T) . f1 = (S * T) . f2 ; :: thesis: f1 = f2
A6: ( (S * T) . f1 = S . (T . f1) & (S * T) . f2 = S . (T . f2) ) by FUNCT_2:15;
( Hom ((T . b),(T . b9)) <> {} & T . f1 is Morphism of T . b,T . b9 ) by A3, Th125, Th126;
then T . f1 = T . f2 by A2, A5, A6, A4, Def24;
hence f1 = f2 by A1, A3, Def24; :: thesis: verum