let C, D be Category; ( 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 #)
; 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; for d being Element of D st c = d holds
id c = id d
let d be Element of D; ( c = d implies id c = id d )
assume A2:
c = d
; 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;
( ( 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 )
( Hom (b,d) <> {} implies for f being Morphism of b,d holds ii (*) f = f )proof
assume A5:
Hom (
d,
b)
<> {}
;
for f being Morphism of d,b holds f (*) ii = f
let f be
Morphism of
d,
b;
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
;
verum
end;
assume A8:
Hom (
b,
d)
<> {}
;
for f being Morphism of b,d holds ii (*) f = f
let f be
Morphism of
b,
d;
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
;
verum
end;
hence
id c = id d
by CAT_1:def 12; verum