let V be non empty set ; for a being Object of (Ens V) st a = {} holds
a is initial
let a be Object of (Ens V); ( a = {} implies a is initial )
assume A1:
a = {}
; a is initial
let b be Object of (Ens V); CAT_1:def 19 ( not Hom (a,b) = {} & ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2 )
Maps ((@ a),(@ b)) <> {}
by A1, Th15;
hence A2:
Hom (a,b) <> {}
by Th26; ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2
set m = [[(@ a),(@ b)],{}];
{} is Function of (@ a),(@ b)
by A1, RELSET_1:12;
then
[[(@ a),(@ b)],{}] in Maps ((@ a),(@ b))
by A1, Th15;
then
[[(@ a),(@ b)],{}] in Hom (a,b)
by Th26;
then reconsider f = [[(@ a),(@ b)],{}] as Morphism of a,b by CAT_1:def 5;
take
f
; for b1 being Morphism of a,b holds f = b1
let g be Morphism of a,b; f = g
reconsider m9 = g as Element of Maps V ;
g in Hom (a,b)
by A2, CAT_1:def 5;
then A3:
g in Maps ((@ a),(@ b))
by Th26;
then A4:
m9 = [[(@ a),(@ b)],(m9 `2)]
by Th16;
then
m9 `2 is Function of (@ a),(@ b)
by A3, Lm4;
hence
f = g
by A1, A4; verum