let C be non empty with_identities CategoryStr ; :: thesis: for f being morphism of C st f is identity holds
f |> f
let f be morphism of C; :: thesis: ( f is identity implies f |> f )
assume f is identity ; :: thesis: f |> f
then f is Object of C by Th22;
hence f |> f by Th23; :: thesis: verum