let a be Element of o Hom ; 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); ( 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:21; 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 ; 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; ( ( 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:22; ( S2[b,a,g] implies H1(f,g) = g )
assume that
A22:
dom g = cod b
and
A23:
g (*) b = a
; H1(f,g) = g
cod g = cod a
by A22, A23, CAT_1:17;
hence
H1(f,g) = g
by CAT_1:21; verum