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