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 18 :: thesis: ( not Hom (b,a) = {} & ex b_{1} being Morphism of b,a st

for b_{2} being Morphism of b,a holds b_{1} = b_{2} )

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; :: thesis: ex b_{1} being Morphism of b,a st

for b_{2} being Morphism of b,a holds b_{1} = b_{2}

[[(@ 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 ; :: thesis: for b_{1} being Morphism of b,a holds f = b_{1}

let g be Morphism of b,a; :: thesis: 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; :: thesis: verum

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 18 :: thesis: ( not Hom (b,a) = {} & ex b

for b

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; :: thesis: ex b

for b

[[(@ 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 ; :: thesis: for b

let g be Morphism of b,a; :: thesis: 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; :: thesis: verum