let C be non empty composable with_identities CategoryStr ; :: thesis: for a, b being Object of C

for f being Morphism of a,b st Hom (a,b) <> {} holds

( f * (id- a) = f & (id- b) * f = f )

let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds

( f * (id- a) = f & (id- b) * f = f )

let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} implies ( f * (id- a) = f & (id- b) * f = f ) )

assume A1: Hom (a,b) <> {} ; :: thesis: ( f * (id- a) = f & (id- b) * f = f )

A3: ( id- a = a & id- b = b ) by CAT_6:def 20;

A4: ( Hom (a,a) <> {} & Hom (b,b) <> {} ) ;

A5: ( f |> id- a & id- b |> f ) by A1, A4, Th17;

thus f * (id- a) = f (*) (id- a) by A4, A1, Def4

.= f by A3, A5, CAT_6:23 ; :: thesis: (id- b) * f = f

thus (id- b) * f = (id- b) (*) f by A4, A1, Def4

.= f by A3, A5, CAT_6:23 ; :: thesis: verum

for f being Morphism of a,b st Hom (a,b) <> {} holds

( f * (id- a) = f & (id- b) * f = f )

let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds

( f * (id- a) = f & (id- b) * f = f )

let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} implies ( f * (id- a) = f & (id- b) * f = f ) )

assume A1: Hom (a,b) <> {} ; :: thesis: ( f * (id- a) = f & (id- b) * f = f )

A3: ( id- a = a & id- b = b ) by CAT_6:def 20;

A4: ( Hom (a,a) <> {} & Hom (b,b) <> {} ) ;

A5: ( f |> id- a & id- b |> f ) by A1, A4, Th17;

thus f * (id- a) = f (*) (id- a) by A4, A1, Def4

.= f by A3, A5, CAT_6:23 ; :: thesis: (id- b) * f = f

thus (id- b) * f = (id- b) (*) f by A4, A1, Def4

.= f by A3, A5, CAT_6:23 ; :: thesis: verum