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 16 :: thesis: ( not Hom a,b = {} & ex b₁ being Morphism of a,b st
for b₂ being Morphism of a,b holds b₁ = b₂ )
set m = [[(@ a),(@ b)],{} ];
{} is Function of (@ a),(@ b) by A1, RELSET_1:25;
then A2: [[(@ a),(@ b)],{} ] in Maps (@ a),(@ b) by A1, Th15;
Maps (@ a),(@ b) <> {} by A1, Th15;
hence A3: Hom a,b <> {} by Th27; :: thesis: ex b₁ being Morphism of a,b st
for b₂ being Morphism of a,b holds b₁ = b₂
[[(@ a),(@ b)],{} ] in Hom a,b by A2, Th27;
then reconsider f = [[(@ a),(@ b)],{} ] as Morphism of a,b by CAT_1:def 7;
take f ; :: thesis: for b₁ being Morphism of a,b holds f = b₁
let g be Morphism of a,b; :: thesis: f = g
g in Hom a,b by A3, CAT_1:def 7;
then A4: g in Maps (@ a),(@ b) by Th27;
Maps (@ a),(@ b) c= Maps V by Th17;
then reconsider m = [[(@ a),(@ b)],{} ], m' = g as Element of Maps V by A2;
A5: m' = [[(@ a),(@ b)],(m' `2 )] by A4, Th16;
m = [[(dom m),(cod m)],(m `2 )] by Th8;
then ( m `2 = {} & m' `2 is Function of (@ a),(@ b) ) by A4, A5, Lm4, ZFMISC_1:33;
hence f = g by A1, A5; :: thesis: verum