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
proof
let o1,
o2 be
Object of
(OrdC 1);
for f1 being morphism of (OrdC 1) holds f1 is Morphism of o1,o2let f1 be
morphism of
(OrdC 1);
f1 is Morphism of o1,o2
A3:
dom f1 =
f
by A1, TARSKI:def 1
.=
o1
by A1, TARSKI:def 1
;
cod f1 =
f
by A1, TARSKI:def 1
.=
o2
by A1, TARSKI:def 1
;
then
f1 in Hom (
o1,
o2)
by A3, CAT_7:20;
hence
f1 is
Morphism of
o1,
o2
by CAT_7:def 3;
verum
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 )
proof
let a,
b be
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 )
set c =
a;
take
a
;
ex e being Morphism of a [x] a,b st
( Hom ((a [x] a),b) <> {} & a,e is_exponent_of a,b )
reconsider e =
f as
Morphism of
a [x] a,
b by A2;
take
e
;
( Hom ((a [x] a),b) <> {} & a,e is_exponent_of a,b )
a [x] a =
f
by A1, TARSKI:def 1
.=
b
by A1, TARSKI:def 1
;
hence A4:
Hom (
(a [x] a),
b)
<> {}
;
a,e is_exponent_of a,b
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 ) ) )
proof
let d be
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 f1 be
Morphism of
d [x] a,
b;
( Hom ((d [x] a),b) <> {} implies ( 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 ) ) ) )
assume
Hom (
(d [x] a),
b)
<> {}
;
( 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 ) ) )
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)
<> {}
;
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 ) )
take
h
;
( f1 = e * (h [x] (id- a)) & ( for h1 being Morphism of d,a st f1 = e * (h1 [x] (id- a)) holds
h = h1 ) )
thus f1 =
f
by A1, TARSKI:def 1
.=
e * (h [x] (id- a))
by A1, TARSKI:def 1
;
for h1 being Morphism of d,a st f1 = e * (h1 [x] (id- a)) holds
h = h1
let h1 be
Morphism of
d,
a;
( f1 = e * (h1 [x] (id- a)) implies h = h1 )
assume
f1 = e * (h1 [x] (id- a))
;
h = h1
thus
h = h1
by A1, TARSKI:def 1;
verum
end;
hence
a,
e is_exponent_of a,
b
by A4, Def29;
verum
end;
hence
OrdC 1 is with_exponential_objects
; verum