let C be Category; :: thesis: for A being MSAlgebra of CatSign the carrier of C st ( for a, b being Object of C holds the Sorts of A . (homsym a,b) = Hom a,b ) holds
for a, b, c being Object of C holds
( Args (compsym a,b,c),A = product <*(Hom b,c),(Hom a,b)*> & Result (compsym a,b,c),A = Hom a,c )
let A be MSAlgebra of CatSign the carrier of C; :: thesis: ( ( for a, b being Object of C holds the Sorts of A . (homsym a,b) = Hom a,b ) implies for a, b, c being Object of C holds
( Args (compsym a,b,c),A = product <*(Hom b,c),(Hom a,b)*> & Result (compsym a,b,c),A = Hom a,c ) )
assume A1: for a, b being Object of C holds the Sorts of A . (homsym a,b) = Hom a,b ; :: thesis: for a, b, c being Object of C holds
( Args (compsym a,b,c),A = product <*(Hom b,c),(Hom a,b)*> & Result (compsym a,b,c),A = Hom a,c )
A2: the carrier of (CatSign the carrier of C) = dom the Sorts of A by PARTFUN1:def 4;
let a, b, c be Object of C; :: thesis: ( Args (compsym a,b,c),A = product <*(Hom b,c),(Hom a,b)*> & Result (compsym a,b,c),A = Hom a,c )
thus Args (compsym a,b,c),A = product (the Sorts of A * (the_arity_of (compsym a,b,c))) by PRALG_2:10
.= product (the Sorts of A * <*(homsym b,c),(homsym a,b)*>) by Def5
.= product <*(the Sorts of A . (homsym b,c)),(the Sorts of A . (homsym a,b))*> by A2, FINSEQ_2:145
.= product <*(Hom b,c),(the Sorts of A . (homsym a,b))*> by A1
.= product <*(Hom b,c),(Hom a,b)*> by A1 ; :: thesis: Result (compsym a,b,c),A = Hom a,c
thus Result (compsym a,b,c),A = the Sorts of A . (the_result_sort_of (compsym a,b,c)) by PRALG_2:10
.= the Sorts of A . (homsym a,c) by Def5
.= Hom a,c by A1 ; :: thesis: verum