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 ;
f = f (*) (id (dom f)) by CAT_1:22;
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:85;
A6: (id a) `12 = c by A2, MCART_1:85;
A7: dom (id a) = b by A5, Th2;
A8: cod (id a) = c by A6, Th2;
A9: b = a by A7;
A10: c = a by A8;
dom h = h `11 by Th2
.= a by A1, MCART_1:85 ;
then h = h (*) (id a) by CAT_1:22
.= [[f,f],((id (dom f)) (*) g)] by A1, A2, A9, A10, Def11
.= [[f,f],g] by A1, A3, A10, CAT_1:21 ;
hence id a = [[a,a],(id (dom f))] by A1, A2, A7, A10; :: thesis: verum