let C be Category; for a, b being Object of C st a is initial holds
( dom (init (a,b)) = a & cod (init (a,b)) = b )
let a, b be Object of C; ( a is initial implies ( dom (init (a,b)) = a & cod (init (a,b)) = b ) )
assume
a is initial
; ( dom (init (a,b)) = a & cod (init (a,b)) = b )
then
Hom (a,b) <> {}
;
hence
( dom (init (a,b)) = a & cod (init (a,b)) = b )
by CAT_1:5; verum