let C be Category; :: thesis: for o being Object of C
for f being Element of Hom o
for a being Object of (C -SliceCat o) st a = f holds
id a = [[a,a],(id (dom f))]
let o be Object of C; :: thesis: for f being Element of Hom o
for a being Object of (C -SliceCat o) st a = f holds
id a = [[a,a],(id (dom f))]
let f be Element of Hom o; :: thesis: for a being Object of (C -SliceCat o) st a = f holds
id a = [[a,a],(id (dom f))]
let a be Object of (C -SliceCat o); :: thesis: ( a = f implies id a = [[a,a],(id (dom f))] )
assume A1: a = f ; :: thesis: id a = [[a,a],(id (dom f))]
consider b, c being Element of Hom o, g being Morphism of C such that
A2: id a = [[b,c],g] and
A3: dom c = cod g and
b = c * g by Def11;
A4: cod (id (dom f)) = dom f by CAT_1:44;
f = f * (id (dom f)) by CAT_1:47;
then reconsider h = [[f,f],(id (dom f))] as Morphism of (C -SliceCat o) by A4, Def11;
A5: (id a) `11 = b by A2, MCART_1:89;
A6: (id a) `12 = c by A2, MCART_1:89;
A7: dom (id a) = b by A5, Th2;
A8: cod (id a) = c by A6, Th2;
A9: b = a by A7, CAT_1:44;
A10: c = a by A8, CAT_1:44;
dom h = h `11 by Th2
.= a by A1, MCART_1:89 ;
then h = h * (id a) by CAT_1:47
.= [[f,f],((id (dom f)) * g)] by A1, A2, A9, A10, Def11
.= [[f,f],g] by A1, A3, A10, CAT_1:46 ;
hence id a = [[a,a],(id (dom f))] by A1, A2, A7, A10, CAT_1:44; :: thesis: verum