let B, C, D be Category; :: thesis: for T being Functor of B,C
for S being Functor of C,D st T is full & S is full holds
S * T is full
let T be Functor of B,C; :: thesis: for S being Functor of C,D st T is full & S is full holds
S * T is full
let S be Functor of C,D; :: thesis: ( T is full & S is full implies S * T is full )
assume that
A1: T is full and
A2: S is full ; :: thesis: S * T is full
let b, b9 be Object of B; :: according to CAT_1:def 26 :: thesis: ( Hom (((S * T) . b),((S * T) . b9)) <> {} implies for g being Morphism of (S * T) . b,(S * T) . b9 holds
( Hom (b,b9) <> {} & ex f being Morphism of b,b9 st g = (S * T) . f ) )
assume A3: Hom (((S * T) . b),((S * T) . b9)) <> {} ; :: thesis: for g being Morphism of (S * T) . b,(S * T) . b9 holds
( Hom (b,b9) <> {} & ex f being Morphism of b,b9 st g = (S * T) . f )
let g be Morphism of (S * T) . b,(S * T) . b9; :: thesis: ( Hom (b,b9) <> {} & ex f being Morphism of b,b9 st g = (S * T) . f )
A4: ( (S * T) . b = S . (T . b) & (S * T) . b9 = S . (T . b9) ) by Th70;
then consider f being Morphism of T . b,T . b9 such that
A5: g = S . f by A2, A3;
A6: Hom ((T . b),(T . b9)) <> {} by A2, A3, A4;
hence Hom (b,b9) <> {} by A1; :: thesis: ex f being Morphism of b,b9 st g = (S * T) . f
consider h being Morphism of b,b9 such that
A7: f = T . h by A1, A6;
take h ; :: thesis: g = (S * T) . h
thus g = (S * T) . h by A5, A7, FUNCT_2:15; :: thesis: verum