let C, D be Category; :: thesis: ( CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) implies for c being Element of C
for d being Element of D st c = d holds
id c = id d )
assume A1: CatStr(# the carrier of C, the carrier' of C, the Source of C, the Target of C, the Comp of C #) = CatStr(# the carrier of D, the carrier' of D, the Source of D, the Target of D, the Comp of D #) ; :: thesis: for c being Element of C
for d being Element of D st c = d holds
id c = id d
let c be Element of C; :: thesis: for d being Element of D st c = d holds
id c = id d
let d be Element of D; :: thesis: ( c = d implies id c = id d )
assume A2: c = d ; :: thesis: id c = id d
reconsider ii = id c as Morphism of D by A1;
A3: cod ii = cod (id c) by A1
.= d by A2 ;
A4: dom ii = dom (id c) by A1
.= d by A2 ;
then reconsider ii = ii as Morphism of d,d by A3, CAT_1:4;
for b being Object of D holds
( ( Hom (d,b) <> {} implies for f being Morphism of d,b holds f (*) ii = f ) & ( Hom (b,d) <> {} implies for f being Morphism of b,d holds ii (*) f = f ) )

proof

let b be Object of D; :: thesis: ( ( Hom (d,b) <> {} implies for f being Morphism of d,b holds f (*) ii = f ) & ( Hom (b,d) <> {} implies for f being Morphism of b,d holds ii (*) f = f ) )
reconsider bb = b as Element of C by A1;
thus ( Hom (d,b) <> {} implies for f being Morphism of d,b holds f (*) ii = f ) :: thesis: ( Hom (b,d) <> {} implies for f being Morphism of b,d holds ii (*) f = f )

proof

assume A5: Hom (d,b) <> {} ; :: thesis: for f being Morphism of d,b holds f (*) ii = f
let f be Morphism of d,b; :: thesis: f (*) ii = f
reconsider ff = f as Morphism of C by A1;
A6: dom ff = dom f by A1
.= c by A2, A5, CAT_1:5 ;
A7: cod (id c) = c
.= dom ff by A6 ;
cod ii = d by A3
.= dom f by A5, CAT_1:5 ;
hence f (*) ii = the Comp of D . (f,ii) by CAT_1:16
.= the Comp of C . (ff,(id c)) by A1
.= ff (*) (id c) by A7, CAT_1:16
.= f by A6, CAT_1:22 ;
:: thesis: verum

end;

assume A8: Hom (b,d) <> {} ; :: thesis: for f being Morphism of b,d holds ii (*) f = f
let f be Morphism of b,d; :: thesis: ii (*) f = f
reconsider ff = f as Morphism of C by A1;
A9: cod ff = cod f by A1
.= c by A2, A8, CAT_1:5 ;
A10: dom (id c) = c
.= cod ff by A9 ;
dom ii = d by A4
.= cod f by A8, CAT_1:5 ;
hence ii (*) f = the Comp of D . (ii,f) by CAT_1:16
.= the Comp of C . ((id c),ff) by A1
.= (id c) (*) ff by A10, CAT_1:16
.= f by A9, CAT_1:21 ;
:: thesis: verum

end;

hence id c = id d by CAT_1:def 12; :: thesis: verum