let a be Element of o Hom ; :: thesis: ex f being Element of the carrier' of C st
( S₂[a,a,f] & ( for b being Element of o Hom
for g being Element of the carrier' of C holds
( ( S₂[a,b,g] implies H₁(g,f) = g ) & ( S₂[b,a,g] implies H₁(f,g) = g ) ) ) )
take f = id (cod a); :: thesis: ( S₂[a,a,f] & ( for b being Element of o Hom
for g being Element of the carrier' of C holds
( ( S₂[a,b,g] implies H₁(g,f) = g ) & ( S₂[b,a,g] implies H₁(f,g) = g ) ) ) )
thus ( dom f = cod a & f (*) a = a ) by CAT_1:21; :: thesis: for b being Element of o Hom
for g being Element of the carrier' of C holds
( ( S₂[a,b,g] implies H₁(g,f) = g ) & ( S₂[b,a,g] implies H₁(f,g) = g ) )
let b be Element of o Hom ; :: thesis: for g being Element of the carrier' of C holds
( ( S₂[a,b,g] implies H₁(g,f) = g ) & ( S₂[b,a,g] implies H₁(f,g) = g ) )
let g be Morphism of C; :: thesis: ( ( S₂[a,b,g] implies H₁(g,f) = g ) & ( S₂[b,a,g] implies H₁(f,g) = g ) )
thus ( dom g = cod a & g (*) a = b implies g (*) f = g ) by CAT_1:22; :: thesis: ( S₂[b,a,g] implies H₁(f,g) = g )
assume that
A22: dom g = cod b and
A23: g (*) b = a ; :: thesis: H₁(f,g) = g
cod g = cod a by A22, A23, CAT_1:17;
hence H₁(f,g) = g by CAT_1:21; :: thesis: verum