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 19 :: thesis: ( not Hom (a,b) = {} & ex b₁ being Morphism of a,b st
for b₂ being Morphism of a,b holds b₁ = b₂ )
set f = the Morphism of a,b;
thus Hom (a,b) <> {} by Th47; :: thesis: ex b₁ being Morphism of a,b st
for b₂ being Morphism of a,b holds b₁ = b₂
take the Morphism of a,b ; :: thesis: for b₁ being Morphism of a,b holds the Morphism of a,b = b₁
thus for b₁ being Morphism of a,b holds the Morphism of a,b = b₁ by Th46; :: thesis: verum