let V be non empty set ; :: thesis: 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); :: thesis: ( ex x being set st a = {x} implies a is terminal )
given x being set such that A1: a = {x} ; :: thesis: a is terminal
let b be Object of (Ens V); :: according to CAT_1:def 15 :: thesis: ( not Hom b,a = {} & ex b₁ being Morphism of b,a st
for b₂ being Morphism of b,a holds b₁ = b₂ )
consider h being Function of (@ b),(@ a);
set m = [[(@ b),(@ a)],h];
A2: [[(@ b),(@ a)],h] in Maps (@ b),(@ a) by A1, Th15;
then [[(@ b),(@ a)],h] in Hom b,a by Th27;
then reconsider f = [[(@ b),(@ a)],h] as Morphism of b,a by CAT_1:def 7;
thus A3: Hom b,a <> {} by A2, Th27; :: thesis: ex b₁ being Morphism of b,a st
for b₂ being Morphism of b,a holds b₁ = b₂
take f ; :: thesis: for b₁ being Morphism of b,a holds f = b₁
let g be Morphism of b,a; :: thesis: f = g
g in Hom b,a by A3, CAT_1:def 7;
then A4: g in Maps (@ b),(@ a) by Th27;
Maps (@ b),(@ a) c= Maps V by Th17;
then reconsider m = [[(@ b),(@ a)],h], m' = g as Element of Maps V by A2;
A5: m' = [[(@ b),(@ a)],(m' `2 )] by A4, Th16;
m = [[(dom m),(cod m)],(m `2 )] by Th8;
then ( m `2 = h & m' `2 is Function of (@ b),(@ a) ) by A4, A5, Lm4, ZFMISC_1:33;
hence f = g by A1, A5, FUNCT_2:66; :: thesis: verum