let X be set ; :: thesis:
let a be Element of (TolCat X); :: thesis:
let aa be Element of TOL X; :: thesis:
assume Z1: a = aa ; :: thesis:
let i be Morphism of a,a; :: thesis:
assume Z2: i = id$ aa ; :: thesis:
let b be Element of (TolCat X); :: thesis:
thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) :: thesis:

proof

assume Z3: Hom (a,b) <> {} ; :: thesis:
let g be Morphism of a,b; :: thesis:
reconsider gg = g as Element of MapsT X ;
Hom (a,a) <> {} ;
then A1: cod i = a by CAT_1:5
.= dom g by Z3, CAT_1:5 ;
A3: dom gg = dom g by Def25
.= aa by Z1, Z3, CAT_1:5 ;
then A2: cod (id$ aa) = dom gg by Th46;
[g,i] in dom the Comp of (TolCat X) by A1, CAT_1:def 6;
hence g (*) i = the Comp of (TolCat X) . (g,i) by CAT_1:def 1
.= gg * (id$ aa) by A2, Z2, Def27
.= g by A3, Th47 ;
:: thesis:

end;

thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) :: thesis:

proof

assume Z3: Hom (b,a) <> {} ; :: thesis:
let g be Morphism of b,a; :: thesis:
reconsider gg = g as Element of MapsT X ;
Hom (a,a) <> {} ;
then A1: dom i = a by CAT_1:5
.= cod g by Z3, CAT_1:5 ;
A3: cod gg = cod g by Def26
.= aa by Z1, Z3, CAT_1:5 ;
then A2: dom (id$ aa) = cod gg by Th46;
[i,g] in dom the Comp of (TolCat X) by A1, CAT_1:def 6;
hence i (*) g = the Comp of (TolCat X) . (i,g) by CAT_1:def 1
.= (id$ aa) * gg by Z2, A2, Def27
.= g by A3, Th47 ;
:: thesis:

end;