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 )

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

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;

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

hence ( dom f = f & cod f = f ) by A1, CAT_6:24, CAT_6:26, CAT_6:27; :: thesis: verum

end;

end;