let C, D be category; :: thesis: ( C is initial & C ~= D implies D is initial )
assume A1: C is initial ; :: thesis: ( not C ~= D or D is initial )
assume C ~= D ; :: thesis: D is initial
then consider F being Functor of C,D, G being Functor of D,C such that
A2: ( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) by CAT_6:def 28;
let B be category; :: according to CAT_8:def 8 :: thesis: ex F being Functor of D,B st
( F is covariant & ( for F1 being Functor of D,B st F1 is covariant holds
F = F1 ) )
consider F1 being Functor of C,B such that
A3: ( F1 is covariant & ( for G being Functor of C,B st G is covariant holds
F1 = G ) ) by A1;
set F2 = F1 (*) G;
take F1 (*) G ; :: thesis: ( F1 (*) G is covariant & ( for F1 being Functor of D,B st F1 is covariant holds
F1 (*) G = F1 ) )
for G1 being Functor of D,B st G1 is covariant holds
F1 (*) G = G1

proof

let G1 be Functor of D,B; :: thesis: ( G1 is covariant implies F1 (*) G = G1 )
assume A4: G1 is covariant ; :: thesis: F1 (*) G = G1
hence F1 (*) G = (G1 (*) F) (*) G by A3, A2, CAT_6:35
.= G1 (*) (F (*) G) by A4, A2, CAT_7:10
.= G1 by A2, A4, CAT_7:11 ;
:: thesis: verum

end;

hence ( F1 (*) G is covariant & ( for F1 being Functor of D,B st F1 is covariant holds
F1 (*) G = F1 ) ) by A2, A3, CAT_6:35; :: thesis: verum