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] & dom c = cod g & b = c * g ) by Def11;
( cod (id (dom f)) = dom f & f = f * (id (dom f)) ) by CAT_1:44, CAT_1:47;
then reconsider h = [[f,f],(id (dom f))] as Morphism of (C -SliceCat o) by Def11;
( (id a) `11 = b & (id a) `12 = c ) by A2, MCART_1:89;
then ( dom (id a) = b & cod (id a) = c ) by Th2;
then A3: ( b = a & c = a ) by 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, A3, Def11
.= [[f,f],g] by A1, A2, A3, CAT_1:46 ;
hence id a = [[a,a],(id (dom f))] by A1, A2, A3; :: thesis: verum