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 b₁ being Morphism of a,b st
for b₂ being Morphism of a,b holds b₁ = b₂ )
consider f being Morphism of a,b;
thus Hom (a,b) <> {} by Th52; :: thesis: ex b₁ being Morphism of a,b st
for b₂ being Morphism of a,b holds b₁ = b₂
take f ; :: thesis: for b₁ being Morphism of a,b holds f = b₁
thus for b₁ being Morphism of a,b holds f = b₁ by Th51; :: thesis: verum