let C, D be category; :: thesis: ( C is terminal & C ~= D implies D is terminal )
assume A1: C is terminal ; :: thesis: ( not C ~= D or D is terminal )
assume C ~= D ; :: thesis: D is terminal
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 4 :: thesis: ex F being Functor of B,D st
( F is covariant & ( for G being Functor of B,D st G is covariant holds
F = G ) )
consider F1 being Functor of B,C such that
A3: ( F1 is covariant & ( for G being Functor of B,C st G is covariant holds
F1 = G ) ) by A1;
set F2 = F (*) F1;
take F (*) F1 ; :: thesis: ( F (*) F1 is covariant & ( for G being Functor of B,D st G is covariant holds
F (*) F1 = G ) )
for G1 being Functor of B,D st G1 is covariant holds
F (*) F1 = G1

proof

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

end;

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