let C1, C2 be Category; :: thesis: ( alter C1 ~= alter C2 implies C1 ~= C2 )
assume alter C1 ~= alter C2 ; :: thesis: C1 ~= C2
then consider F being Functor of (alter C1),(alter C2), G being Functor of (alter C2),(alter C1) such that
A1: ( F is covariant & G is covariant & G (*) F = id (alter C1) & F (*) G = id (alter C2) ) ;
reconsider F1 = F as Functor of C1,C2 by A1, Th49;
A2: dom F = the carrier of (alter C1) by FUNCT_2:def 1;
G (*) F = F * G by A1, Def27;
then F * G = id the carrier of (alter C1) by A1, STRUCT_0:def 4;
then A3: F is one-to-one by A2, FUNCT_1:31;
A4: F (*) G = G * F by A1, Def27;
A5: the carrier' of C2 = rng (id the carrier' of C2)
.= rng (G * F) by A4, A1, STRUCT_0:def 4 ;
the carrier' of C2 c= rng F by A5, RELAT_1:26;
then rng F1 = the carrier' of C2 by XBOOLE_0:def 10;
hence C1 ~= C2 by A3, ISOCAT_1:def 4, ISOCAT_1:def 3; :: thesis: verum