let a be Element of Hom o; :: thesis: ex f being Element of the carrier' of C st
( S₁[a,a,f] & ( for b being Element of Hom o
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 (dom a); :: thesis: ( S₁[a,a,f] & ( for b being Element of Hom o
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 a = cod f & a = a (*) f ) by CAT_1:22; :: thesis: for b being Element of Hom o
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 Hom o; :: 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 ) )

hereby :: thesis: ( S₁[b,a,g] implies H₁(f,g) = g )

assume that
A7: dom b = cod g and
A8: a = b (*) g ; :: thesis: g (*) f = g
dom a = dom g by A7, A8, CAT_1:17;
hence g (*) f = g by CAT_1:22; :: thesis: verum

end;

thus ( S₁[b,a,g] implies H₁(f,g) = g ) by CAT_1:21; :: thesis: verum