let C be Category; :: thesis: 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; :: thesis: ( a is initial implies ( dom (init (a,b)) = a & cod (init (a,b)) = b ) )

assume a is initial ; :: thesis: ( 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; :: thesis: verum

( dom (init (a,b)) = a & cod (init (a,b)) = b )

let a, b be Object of C; :: thesis: ( a is initial implies ( dom (init (a,b)) = a & cod (init (a,b)) = b ) )

assume a is initial ; :: thesis: ( 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; :: thesis: verum