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;

for a, b being Object of (OrdC 1) ex c being Object of (OrdC 1) ex e being Morphism of c [x] a,b st
( Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b )

let a, b be Object of (OrdC 1); :: thesis:
set c = a;
take a ; :: thesis:
reconsider e = f as Morphism of a [x] a,b by A2;
take e ; :: thesis:
a [x] a = f by A1, TARSKI:def 1
.= b by A1, TARSKI:def 1 ;
hence A4: Hom ((a [x] a),b) <> {} ; :: thesis:
for d being Object of (OrdC 1)
for f1 being Morphism of d [x] a,b st Hom ((d [x] a),b) <> {} holds
( Hom (d,a) <> {} & ex h being Morphism of d,a st
( f1 = e * (h [x] (id- a)) & ( for h1 being Morphism of d,a st f1 = e * (h1 [x] (id- a)) holds
h = h1 ) ) )

let d be Object of (OrdC 1); :: thesis:
let f1 be Morphism of d [x] a,b; :: thesis:
assume Hom ((d [x] a),b) <> {} ; :: thesis:
reconsider h = f as Morphism of d,a by A2;
d = f by A1, TARSKI:def 1
.= a by A1, TARSKI:def 1 ;
hence Hom (d,a) <> {} ; :: thesis:
take h ; :: thesis:
thus f1 = f by A1, TARSKI:def 1
.= e * (h [x] (id- a)) by A1, TARSKI:def 1 ; :: thesis:
let h1 be Morphism of d,a; :: thesis:
assume f1 = e * (h1 [x] (id- a)) ; :: thesis:
thus h = h1 by A1, TARSKI:def 1; :: thesis:

end;

end;