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 A6:
( dom f = cod a & f * a = b & dom g = cod b & g * b = c )
; :: thesis: ( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] )
then
dom g = cod f
by CAT_1:42;
hence
( H1(g,f) in the carrier' of C & S2[a,c,H1(g,f)] )
by A6, CAT_1:42, CAT_1:43; :: thesis: verum