let a, b, c be Element of o Hom ; :: thesis: for f, g being Element of the carrier' of C st S2[a,b,f] & S2[b,c,g] holds
( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] )
let f, g be Morphism of C; :: thesis: ( S2[a,b,f] & S2[b,c,g] implies ( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] ) )
assume that
A17: dom f = cod a and
A18: f (*) a = b and
A19: dom g = cod b and
A20: g (*) b = c ; :: thesis: ( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] )
dom g = cod f by A17, A18, A19, CAT_1:17;
hence ( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] ) by A17, A18, A20, CAT_1:17, CAT_1:18; :: thesis: verum