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 ( dom b = cod f & a = b * f & dom c = cod g & b = c * g & dom d = cod h & c = d * h ) ; :: thesis: H₁(h,H₁(g,f)) = H₁(H₁(h,g),f)
then ( dom g = cod f & dom h = cod g ) by CAT_1:42;
hence H₁(h,H₁(g,f)) = H₁(H₁(h,g),f) by CAT_1:43; :: thesis: verum