let o, m be set ; :: thesis: for a being Object of (c1Cat* o,m) holds a is initial
let a be Object of (c1Cat* o,m); :: thesis: a is initial
let b be Object of (c1Cat* o,m); :: according to CAT_1:def 16 :: thesis: ( not Hom a,b = {} & ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2 )
consider f being Morphism of a,b;
thus Hom a,b <> {} by Th52; :: thesis: ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2
take f ; :: thesis: for b1 being Morphism of a,b holds f = b1
thus for b1 being Morphism of a,b holds f = b1 by Th51; :: thesis: verum