let C be non empty with_identities CategoryStr ; :: thesis: for f being morphism of C ex f1, f2 being morphism of C st
( f1 is identity & f2 is identity & f1 |> f & f |> f2 )
let f be morphism of C; :: thesis: ex f1, f2 being morphism of C st
( f1 is identity & f2 is identity & f1 |> f & f |> f2 )
f in Mor C ;
then A1: f in the carrier of C by CAT_6:def 1;
then consider f1 being morphism of C such that
A2: ( f1 |> f & f1 is left_identity ) by CAT_6:def 6, CAT_6:def 12;
consider f2 being morphism of C such that
A3: ( f |> f2 & f2 is right_identity ) by A1, CAT_6:def 7, CAT_6:def 12;
take f1 ; :: thesis: ex f2 being morphism of C st
( f1 is identity & f2 is identity & f1 |> f & f |> f2 )
take f2 ; :: thesis: ( f1 is identity & f2 is identity & f1 |> f & f |> f2 )
f1 is right_identity by A2, CAT_6:9;
hence f1 is identity by A2, CAT_6:def 14; :: thesis: ( f2 is identity & f1 |> f & f |> f2 )
f2 is left_identity by A3, CAT_6:9;
hence f2 is identity by A3, CAT_6:def 14; :: thesis: ( f1 |> f & f |> f2 )
thus ( f1 |> f & f |> f2 ) by A2, A3; :: thesis: verum