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₂ )
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₂
consider f being Morphism of a,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