let C be Category; :: thesis: for o being Object of C
for f being Element of o Hom
for a being Object of (o -SliceCat C) st a = f holds
id a = [[a,a],(id (cod f))]
let o be Object of C; :: thesis: for f being Element of o Hom
for a being Object of (o -SliceCat C) st a = f holds
id a = [[a,a],(id (cod f))]
let f be Element of o Hom ; :: thesis: for a being Object of (o -SliceCat C) st a = f holds
id a = [[a,a],(id (cod f))]
let a be Object of (o -SliceCat C); :: thesis: ( a = f implies id a = [[a,a],(id (cod f))] )
assume A1: a = f ; :: thesis: id a = [[a,a],(id (cod f))]
consider b, c being Element of o Hom , g being Morphism of C such that
A2: id a = [[b,c],g] and
A3: dom g = cod b and
g (*) b = c by Def12;
A4: dom (id (cod f)) = cod f ;
f = (id (cod f)) (*) f by CAT_1:21;
then reconsider h = [[f,f],(id (cod f))] as Morphism of (o -SliceCat C) by A4, Def12;
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;
cod h = h `12 by Th2
.= a by A1, MCART_1:85 ;
then h = (id a) (*) h by CAT_1:21
.= [[f,f],(g (*) (id (cod f)))] by A1, A2, A9, A10, Def12
.= [[f,f],g] by A1, A3, A9, CAT_1:22 ;
hence id a = [[a,a],(id (cod f))] by A1, A2, A8, A9; :: thesis: verum