let a be Element of Hom o; :: thesis: ex f being Element of the carrier' of C st
( S1[a,a,f] & ( for b being Element of Hom o
for g being Element of the carrier' of C holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) ) ) )
take f = id (dom a); :: thesis: ( S1[a,a,f] & ( for b being Element of Hom o
for g being Element of the carrier' of C holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(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
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) )
let b be Element of Hom o; :: thesis: for g being Element of the carrier' of C holds
( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) )
let g be Morphism of C; :: thesis: ( ( S1[a,b,g] implies H1(g,f) = g ) & ( S1[b,a,g] implies H1(f,g) = g ) )
hereby :: thesis: ( S1[b,a,g] implies H1(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 ( S1[b,a,g] implies H1(f,g) = g ) by CAT_1:21; :: thesis: verum