let C be non empty category; for o1 being Object of C
for o2 being Object of (Alter C) st o1 = o2 holds
id- o1 = id o2
let o1 be Object of C; for o2 being Object of (Alter C) st o1 = o2 holds
id- o1 = id o2
let o2 be Object of (Alter C); ( o1 = o2 implies id- o1 = id o2 )
assume A1:
o1 = o2
; id- o1 = id o2
A2:
o1 in Ob C
;
then reconsider f1 = o1 as morphism of C ;
reconsider a2 = o2 as Morphism of (Alter C) by A1, A2;
A3:
( f1 is identity & f1 |> f1 )
by Th22, Th24;
A4: dom a2 =
dom f1
by A1, Th45
.=
o2
by A1, A3, Def18
;
A5: cod a2 =
cod f1
by A1, Th45
.=
o2
by A1, A3, Def19
;
reconsider a3 = a2 as Morphism of o2,o2 by A4, A5, CAT_1:4;
for b being Object of (Alter C) holds
( ( Hom (o2,b) <> {} implies for a being Morphism of o2,b holds a (*) a3 = a ) & ( Hom (b,o2) <> {} implies for a being Morphism of b,o2 holds a3 (*) a = a ) )
proof
let b be
Object of
(Alter C);
( ( Hom (o2,b) <> {} implies for a being Morphism of o2,b holds a (*) a3 = a ) & ( Hom (b,o2) <> {} implies for a being Morphism of b,o2 holds a3 (*) a = a ) )
thus
(
Hom (
o2,
b)
<> {} implies for
a being
Morphism of
o2,
b holds
a (*) a3 = a )
( Hom (b,o2) <> {} implies for a being Morphism of b,o2 holds a3 (*) a = a )proof
assume A6:
Hom (
o2,
b)
<> {}
;
for a being Morphism of o2,b holds a (*) a3 = a
let a be
Morphism of
o2,
b;
a (*) a3 = a
reconsider f2 =
a as
morphism of
C ;
dom a = cod a3
by A5, A6, CAT_1:5;
then A7:
[f2,f1] in dom the
composition of
C
by A1, CAT_1:15;
thus a (*) a3 =
f2 (*) f1
by A1, A7, Def2, Th44
.=
a
by A3, A7, Def2, Def5
;
verum
end;
assume A8:
Hom (
b,
o2)
<> {}
;
for a being Morphism of b,o2 holds a3 (*) a = a
let a be
Morphism of
b,
o2;
a3 (*) a = a
reconsider f2 =
a as
morphism of
C ;
dom a3 = cod a
by A4, A8, CAT_1:5;
then A9:
[f1,f2] in dom the
composition of
C
by A1, CAT_1:15;
thus a3 (*) a =
f1 (*) f2
by A1, A9, Def2, Th44
.=
a
by A3, A9, Def2, Def4
;
verum
end;
hence
id- o1 = id o2
by A1, CAT_1:def 12; verum