let A be Category; :: thesis: for f, g being Function
for m1, m2 being Morphism of (EnsHom A) st cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 holds
[[(dom m1),(cod m2)],(g * f)] = m2 * m1
let f, g be Function; :: thesis: for m1, m2 being Morphism of (EnsHom A) st cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 holds
[[(dom m1),(cod m2)],(g * f)] = m2 * m1
let m1, m2 be Morphism of (EnsHom A); :: thesis: ( cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 implies [[(dom m1),(cod m2)],(g * f)] = m2 * m1 )
assume that
A1: cod m1 = dom m2 and
A2: [[(dom m1),(cod m1)],f] = m1 and
A3: [[(dom m2),(cod m2)],g] = m2 ; :: thesis: [[(dom m1),(cod m2)],(g * f)] = m2 * m1
A4: EnsHom A = CatStr(# (Hom A),(Maps (Hom A)),(fDom (Hom A)),(fCod (Hom A)),(fComp (Hom A)),(fId (Hom A)) #) by ENS_1:def 14;
then reconsider m19 = m1 as Element of Maps (Hom A) ;
reconsider m29 = m2 as Element of Maps (Hom A) by A4;
A5: cod m19 = (m1 `1) `2 by ENS_1:def 5
.= [(dom m1),(cod m1)] `2 by A2, MCART_1:7
.= dom m2 by A1, MCART_1:7
.= [(dom m2),(cod m2)] `1 by MCART_1:7
.= (m2 `1) `1 by A3, MCART_1:7
.= dom m29 by ENS_1:def 4 ;
[[(dom m19),(cod m19)],(m19 `2)] = m1 by ENS_1:8;
then A6: m19 `2 = f by A2, ZFMISC_1:33;
[[(dom m29),(cod m29)],(m29 `2)] = m2 by ENS_1:8;
then A7: m29 `2 = g by A3, ZFMISC_1:33;
A8: cod m2 = [(dom m2),(cod m2)] `2 by MCART_1:7
.= (m2 `1) `2 by A3, MCART_1:7
.= cod m29 by ENS_1:def 5 ;
A9: dom m19 = (m1 `1) `1 by ENS_1:def 4
.= [(dom m1),(cod m1)] `1 by A2, MCART_1:7
.= dom m1 by MCART_1:7 ;
[m2,m1] in dom the Comp of (EnsHom A) by A1, CAT_1:40;
then m2 * m1 = (fComp (Hom A)) . (m29,m19) by A4, CAT_1:def 4
.= m29 * m19 by A5, ENS_1:def 12
.= [[(dom m1),(cod m2)],(g * f)] by A5, A9, A8, A7, A6, ENS_1:def 7 ;
hence [[(dom m1),(cod m2)],(g * f)] = m2 * m1 ; :: thesis: verum