let C be Category; :: thesis: 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 )
let o be Object of C; :: thesis: for m being Morphism of (o -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 )
let m be Morphism of (o -SliceCat C); :: thesis: ( 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 )
consider a, b being Element of o Hom , f being Morphism of C such that
A1: ( m = [[a,b],f] & dom f = cod a & f * a = b ) by Def12;
( m `11 = a & m `12 = b & m `2 = f ) by A1, MCART_1:7, MCART_1:89;
hence ( 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 ) by A1, Th2; :: thesis: verum