let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of C st f in Hom a,b holds
( (Den (compsym a,b,b),(MSAlg C)) . <*(id b),f*> = f & (Den (compsym a,a,b),(MSAlg C)) . <*f,(id a)*> = f )
let a, b be Object of C; :: thesis: for f being Morphism of C st f in Hom a,b holds
( (Den (compsym a,b,b),(MSAlg C)) . <*(id b),f*> = f & (Den (compsym a,a,b),(MSAlg C)) . <*f,(id a)*> = f )
let f be Morphism of C; :: thesis: ( f in Hom a,b implies ( (Den (compsym a,b,b),(MSAlg C)) . <*(id b),f*> = f & (Den (compsym a,a,b),(MSAlg C)) . <*f,(id a)*> = f ) )
assume A1: f in Hom a,b ; :: thesis: ( (Den (compsym a,b,b),(MSAlg C)) . <*(id b),f*> = f & (Den (compsym a,a,b),(MSAlg C)) . <*f,(id a)*> = f )
then dom f = a by CAT_1:18;
then A2: f * (id a) = f by CAT_1:47;
cod f = b by A1, CAT_1:18;
then A3: (id b) * f = f by CAT_1:46;
( id b in Hom b,b & id a in Hom a,a ) by CAT_1:55;
hence ( (Den (compsym a,b,b),(MSAlg C)) . <*(id b),f*> = f & (Den (compsym a,a,b),(MSAlg C)) . <*f,(id a)*> = f ) by A1, A3, A2, Th42; :: thesis: verum