let C be Category; :: thesis: for a being Object of C
for m being Morphism of (C -SliceCat a) holds
( m = [[(m `11 ),(m `12 )],(m `2 )] & dom (m `12 ) = cod (m `2 ) & m `11 = (m `12 ) * (m `2 ) & dom m = m `11 & cod m = m `12 )
let o be Object of C; :: thesis: for m being Morphism of (C -SliceCat o) holds
( m = [[(m `11 ),(m `12 )],(m `2 )] & dom (m `12 ) = cod (m `2 ) & m `11 = (m `12 ) * (m `2 ) & dom m = m `11 & cod m = m `12 )
let m be Morphism of (C -SliceCat o); :: thesis: ( m = [[(m `11 ),(m `12 )],(m `2 )] & dom (m `12 ) = cod (m `2 ) & m `11 = (m `12 ) * (m `2 ) & dom m = m `11 & cod m = m `12 )
consider a, b being Element of Hom o, f being Morphism of C such that
A1: m = [[a,b],f] and
A2: dom b = cod f and
A3: a = b * f by Def11;
A4: m `11 = a by A1, MCART_1:89;
m `12 = b by A1, MCART_1:89;
hence ( m = [[(m `11 ),(m `12 )],(m `2 )] & dom (m `12 ) = cod (m `2 ) & m `11 = (m `12 ) * (m `2 ) & dom m = m `11 & cod m = m `12 ) by A1, A2, A3, A4, Th2, MCART_1:7; :: thesis: verum