let A be Category; :: thesis: for a, b, c being Object of A holds
( Args (compsym a,b,c),(MSAlg A) = product <*(Hom b,c),(Hom a,b)*> & Result (compsym a,b,c),(MSAlg A) = Hom a,c )
let a, b, c be Object of A; :: thesis: ( Args (compsym a,b,c),(MSAlg A) = product <*(Hom b,c),(Hom a,b)*> & Result (compsym a,b,c),(MSAlg A) = Hom a,c )
for a, b being Object of A holds the Sorts of (MSAlg A) . (homsym a,b) = Hom a,b by Def15;
hence ( Args (compsym a,b,c),(MSAlg A) = product <*(Hom b,c),(Hom a,b)*> & Result (compsym a,b,c),(MSAlg A) = Hom a,c ) by Lm3; :: thesis: verum