set C = OrdC 1;
consider f being morphism of (OrdC 1) such that
A1: ( f is identity & Ob (OrdC 1) = {f} & Mor (OrdC 1) = {f} ) by Th15;
A2: for o1, o2 being Object of (OrdC 1)
for f1 being morphism of (OrdC 1) holds f1 is Morphism of o1,o2

end;

let a, b be Object of (OrdC 1); :: according to CAT_8:def 11 :: thesis:
A4: a = f by A1, TARSKI:def 1
.= b by A1, TARSKI:def 1 ;
take a ; :: thesis:
reconsider p1 = f as Morphism of a,a by A2;
reconsider p2 = f as Morphism of a,b by A2;
take p1 ; :: thesis:
take p2 ; :: thesis:
thus A5: ( Hom (a,a) <> {} & Hom (a,b) <> {} ) by A4; :: thesis:
for c1 being Object of (OrdC 1)
for q1 being Morphism of c1,a
for q2 being Morphism of c1,b st Hom (c1,a) <> {} & Hom (c1,b) <> {} holds
( Hom (c1,a) <> {} & ex h being Morphism of c1,a st
( p1 * h = q1 & p2 * h = q2 & ( for h1 being Morphism of c1,a st p1 * h1 = q1 & p2 * h1 = q2 holds
h = h1 ) ) )

let c1 be Object of (OrdC 1); :: thesis:
let q1 be Morphism of c1,a; :: thesis:
let q2 be Morphism of c1,b; :: thesis:
assume ( Hom (c1,a) <> {} & Hom (c1,b) <> {} ) ; :: thesis:
c1 = f by A1, TARSKI:def 1
.= a by A1, TARSKI:def 1 ;
hence Hom (c1,a) <> {} ; :: thesis:
reconsider h = f as Morphism of c1,a by A2;
take h ; :: thesis:
thus p1 * h = f by A1, TARSKI:def 1
.= q1 by A1, TARSKI:def 1 ; :: thesis:
thus p2 * h = f by A1, TARSKI:def 1
.= q2 by A1, TARSKI:def 1 ; :: thesis:
let h1 be Morphism of c1,a; :: thesis:
assume ( p1 * h1 = q1 & p2 * h1 = q2 ) ; :: thesis:
thus h = h1 by A1, TARSKI:def 1; :: thesis:

end;