for C being Category
for a being Object of C
for m being Morphism of (a -SliceCat C) holds
( m = [[(m `11),(m `12)],(m `2)] & dom (m `2) = cod (m `11) & (m `2) (*) (m `11) = m `12 & dom m = m `11 & cod m = m `12 )