let C be composable with_identities CategoryStr ; :: thesis: for f being morphism of C st f is identity holds

( dom f = f & cod f = f )

let f be morphism of C; :: thesis: ( f is identity implies ( dom f = f & cod f = f ) )

assume A1: f is identity ; :: thesis: ( dom f = f & cod f = f )

( dom f = f & cod f = f )

let f be morphism of C; :: thesis: ( f is identity implies ( dom f = f & cod f = f ) )

assume A1: f is identity ; :: thesis: ( dom f = f & cod f = f )

per cases
( C is empty or not C is empty )
;

end;

suppose A2:
C is empty
; :: thesis: ( dom f = f & cod f = f )

then A3:
the Object of C = {}
by SUBSET_1:def 1;

( dom f = the Object of C & cod f = the Object of C ) by A2, CAT_6:def 18, CAT_6:def 19;

hence ( dom f = f & cod f = f ) by A3, A2, SUBSET_1:def 1; :: thesis: verum

end;( dom f = the Object of C & cod f = the Object of C ) by A2, CAT_6:def 18, CAT_6:def 19;

hence ( dom f = f & cod f = f ) by A3, A2, SUBSET_1:def 1; :: thesis: verum