let C be composable with_identities CategoryStr ; :: thesis: for f, f1 being morphism of C st f1 |> f & f1 is identity holds
cod f = f1
let f, f1 be morphism of C; :: thesis: ( f1 |> f & f1 is identity implies cod f = f1 )
assume A1: ( f1 |> f & f1 is identity ) ; :: thesis: cod 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 & f11 |> f & f11 is identity ) by A1;
hence cod f = f1 by A2, Def19; :: thesis: verum