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)) #) by ENS_1:def 13;
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 4
.= [(dom m1),(cod m1)] `2 by A2
.= dom m2 by A1
.= [(dom m2),(cod m2)] `1
.= (m2 `1) `1 by A3
.= dom m29 by ENS_1:def 3 ;
A6: m19 `2 = f by A2;
A7: m29 `2 = g by A3;
A8: cod m2 = [(dom m2),(cod m2)] `2
.= (m2 `1) `2 by A3
.= cod m29 by ENS_1:def 4 ;
A9: dom m19 = (m1 `1) `1 by ENS_1:def 3
.= [(dom m1),(cod m1)] `1 by A2
.= dom m1 ;
[m2,m1] in dom the Comp of (EnsHom A) by A1, CAT_1:15;
then m2 (*) m1 = (fComp (Hom A)) . (m29,m19) by A4, CAT_1:def 1
.= m29 * m19 by A5, ENS_1:def 11
.= [[(dom m1),(cod m2)],(g * f)] by A5, A9, A8, A7, A6, ENS_1:def 6 ;
hence [[(dom m1),(cod m2)],(g * f)] = m2 (*) m1 ; :: thesis: verum