let a, b, c, d be Element of o Hom ; for f, g, h being Element of the carrier' of C st S2[a,b,f] & S2[b,c,g] & S2[c,d,h] holds
H1(h,H1(g,f)) = H1(H1(h,g),f)
let f, g, h be Morphism of C; ( S2[a,b,f] & S2[b,c,g] & S2[c,d,h] implies H1(h,H1(g,f)) = H1(H1(h,g),f) )
assume that
A25:
dom f = cod a
and
A26:
f (*) a = b
and
A27:
dom g = cod b
and
A28:
g (*) b = c
and
A29:
dom h = cod c
and
h (*) c = d
; H1(h,H1(g,f)) = H1(H1(h,g),f)
A30:
dom g = cod f
by A25, A26, A27, CAT_1:17;
dom h = cod g
by A27, A28, A29, CAT_1:17;
hence
H1(h,H1(g,f)) = H1(H1(h,g),f)
by A30, CAT_1:18; verum