let V be non empty set ; :: thesis: for a being Object of (Ens V) st a = {} holds

a is initial

let a be Object of (Ens V); :: thesis: ( a = {} implies a is initial )

assume A1: a = {} ; :: thesis: a is initial

let b be Object of (Ens V); :: according to CAT_1:def 19 :: thesis: ( not Hom (a,b) = {} & ex b_{1} being Morphism of a,b st

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

Maps ((@ a),(@ b)) <> {} by A1, Th15;

hence A2: Hom (a,b) <> {} by Th26; :: thesis: ex b_{1} being Morphism of a,b st

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

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

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

a is initial

let a be Object of (Ens V); :: thesis: ( a = {} implies a is initial )

assume A1: a = {} ; :: thesis: a is initial

let b be Object of (Ens V); :: according to CAT_1:def 19 :: thesis: ( not Hom (a,b) = {} & ex b

for b

Maps ((@ a),(@ b)) <> {} by A1, Th15;

hence A2: Hom (a,b) <> {} by Th26; :: thesis: ex b

for b

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

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