let a be Element of o Hom ; :: thesis: ex f being Element of the carrier' of C st
( S2[a,a,f] & ( for b being Element of o Hom
for g being Element of the carrier' of C holds
( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) ) ) )
take f = id (cod a); :: thesis: ( S2[a,a,f] & ( for b being Element of o Hom
for g being Element of the carrier' of C holds
( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) ) ) )
thus ( dom f = cod a & f * a = a ) by CAT_1:44, CAT_1:46; :: thesis: for b being Element of o Hom
for g being Element of the carrier' of C holds
( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) )
let b be Element of o Hom ; :: thesis: for g being Element of the carrier' of C holds
( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) )
let g be Morphism of C; :: thesis: ( ( S2[a,b,g] implies H1(g,f) = g ) & ( S2[b,a,g] implies H1(f,g) = g ) )
thus ( dom g = cod a & g * a = b implies g * f = g ) by CAT_1:47; :: thesis: ( S2[b,a,g] implies H1(f,g) = g )
assume that
A22: dom g = cod b and
A23: g * b = a ; :: thesis: H1(f,g) = g
cod g = cod a by A22, A23, CAT_1:42;
hence H1(f,g) = g by CAT_1:46; :: thesis: verum