let a, b, c, d be Element of Hom o; :: thesis: for f, g, h being Element of the carrier' of C st S₁[a,b,f] & S₁[b,c,g] & S₁[c,d,h] holds
H₁(h,H₁(g,f)) = H₁(H₁(h,g),f)
let f, g, h be Morphism of C; :: thesis: ( S₁[a,b,f] & S₁[b,c,g] & S₁[c,d,h] implies H₁(h,H₁(g,f)) = H₁(H₁(h,g),f) )
assume that
A10: dom b = cod f and
a = b (*) f and
A11: dom c = cod g and
A12: b = c (*) g and
A13: dom d = cod h and
A14: c = d (*) h ; :: thesis: H₁(h,H₁(g,f)) = H₁(H₁(h,g),f)
A15: dom g = cod f by A10, A11, A12, CAT_1:17;
dom h = cod g by A11, A13, A14, CAT_1:17;
hence H₁(h,H₁(g,f)) = H₁(H₁(h,g),f) by A15, CAT_1:18; :: thesis: verum