let a, b, c be Element of Hom o; :: thesis: for f, g being Element of the carrier' of C st S₁[a,b,f] & S₁[b,c,g] holds
( H₁(g,f) in the carrier' of C & S₁[a,c,H₁(g,f)] )
let f, g be Morphism of C; :: thesis: ( S₁[a,b,f] & S₁[b,c,g] implies ( H₁(g,f) in the carrier' of C & S₁[a,c,H₁(g,f)] ) )
assume that
A2: dom b = cod f and
A3: a = b (*) f and
A4: dom c = cod g and
A5: b = c (*) g ; :: thesis: ( H₁(g,f) in the carrier' of C & S₁[a,c,H₁(g,f)] )
dom g = cod f by A2, A4, A5, CAT_1:17;
hence ( H₁(g,f) in the carrier' of C & S₁[a,c,H₁(g,f)] ) by A3, A4, A5, CAT_1:17, CAT_1:18; :: thesis: verum