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:1;
then A2: f (*) (id a) = f by CAT_1:22;
cod f = b by A1, CAT_1:1;
then A3: (id b) (*) f = f by CAT_1:21;
( id b in Hom (b,b) & id a in Hom (a,a) ) by CAT_1:27;
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, Th31; :: thesis: verum