for C being Category
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))]