let C be composable with_identities CategoryStr ; :: thesis: for f, f1 being morphism of C st f |> f1 & f1 is identity holds
dom f = f1
let f, f1 be morphism of C; :: thesis: ( f |> f1 & f1 is identity implies dom f = f1 )
assume A1: ( f |> f1 & f1 is identity ) ; :: thesis: dom f = f1
then A2: not C is empty ;
then reconsider o = f1 as Object of C by A1, Th22;
ex f11 being morphism of C st
( o = f11 & f |> f11 & f11 is identity ) by A1;
hence dom f = f1 by A2, Def18; :: thesis: verum