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