let A be Category; 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; 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); ( 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
; [[(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
; verum