let C, D be with_identities CategoryStr ; :: thesis: ( C ~= D implies ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) ) )
assume C ~= D ; :: thesis: ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) )
then consider F being Functor of C,D, G being Functor of D,C such that
A1: ( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) by CAT_6:def 28;
F * G = id C by A1, CAT_6:def 27
.= id the carrier of C by STRUCT_0:def 4 ;
then A2: F is one-to-one by FUNCT_2:23;
A3: G * F = id D by A1, CAT_6:def 27
.= id the carrier of D by STRUCT_0:def 4 ;

per cases ( D is empty or not D is empty ) ;

suppose A4: D is empty ; :: thesis: ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) )

C is empty by A4, A1, CAT_6:31;
hence ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) ) by A4; :: thesis: verum

end;

suppose A5: not D is empty ; :: thesis: ( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) )

F is onto by A3, FUNCT_2:23;
then rng F = the carrier of D by FUNCT_2:def 3;
then A6: rng F = Mor D by CAT_6:def 1;
A7: dom F = the carrier of C by A5, FUNCT_2:def 1;
then A8: dom F = Mor C by CAT_6:def 1;
hence card (Mor C) = card (Mor D) by CARD_1:5, A6, A2, WELLORD2:def 4; :: thesis: card (Ob C) = card (Ob D)
set F1 = F | (Ob C);
A9: dom (F | (Ob C)) = Ob C by A8, RELAT_1:62;
for y being object holds
( y in rng (F | (Ob C)) iff y in Ob D )

proof

let y be object ; :: thesis: ( y in rng (F | (Ob C)) iff y in Ob D )

hereby :: thesis: ( y in Ob D implies y in rng (F | (Ob C)) )

assume y in rng (F | (Ob C)) ; :: thesis: y in Ob D
then consider x being object such that
A10: ( x in dom (F | (Ob C)) & y = (F | (Ob C)) . x ) by FUNCT_1:def 3;
A11: x in Ob C by A10;
A12: y = F . x by A10, FUNCT_1:49;
x in { f where f is morphism of C : ( f is identity & f in Mor C ) } by A11, CAT_6:def 17;
then consider f being morphism of C such that
A13: ( x = f & f is identity & f in Mor C ) ;
not C is empty by A10;
then A14: y = F . f by A12, A13, CAT_6:def 21;
then reconsider g = y as morphism of D ;
Mor D <> {} by A5;
then ( g is identity & g in Mor D ) by A14, A13, CAT_6:def 22, A1, CAT_6:def 25;
then g in { f1 where f1 is morphism of D : ( f1 is identity & f1 in Mor D ) } ;
hence y in Ob D by CAT_6:def 17; :: thesis: verum

end;

assume y in Ob D ; :: thesis: y in rng (F | (Ob C))
then y in { g where g is morphism of D : ( g is identity & g in Mor D ) } by CAT_6:def 17;
then consider g being morphism of D such that
A15: ( y = g & g is identity & g in Mor D ) ;
consider x being object such that
A16: ( x in dom F & g = F . x ) by A15, A6, FUNCT_1:def 3;
reconsider f = x as morphism of C by A16, CAT_6:def 1;
A17: not C is empty by A16;
then g = F . f by A16, CAT_6:def 21;
then G . g = (G (*) F) . f by A1, A17, CAT_6:34
.= (id C) . x by A1, A17, CAT_6:def 21
.= (id the carrier of C) . x by STRUCT_0:def 4
.= x by FUNCT_1:18, A16 ;
then ( f is identity & f in Mor C ) by A16, A7, A15, CAT_6:def 22, A1, CAT_6:def 25, CAT_6:def 1;
then f in { f1 where f1 is morphism of C : ( f1 is identity & f1 in Mor C ) } ;
then A18: f in Ob C by CAT_6:def 17;
g = (F | (Ob C)) . f by A18, A16, FUNCT_1:49;
hence y in rng (F | (Ob C)) by A9, A18, A15, FUNCT_1:def 3; :: thesis: verum

end;

then A19: rng (F | (Ob C)) = Ob D by TARSKI:2;
F | (Ob C) is one-to-one by A2, FUNCT_1:52;
hence card (Ob C) = card (Ob D) by CARD_1:5, A9, A19, WELLORD2:def 4; :: thesis: verum

end;

end;