let C be Category; :: thesis: for A being MSAlgebra over 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 over 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) )
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) )
A2: the carrier of (CatSign the carrier of C) = dom the Sorts of A by PARTFUN1:def 2;
thus Args ((compsym (a,b,c)),A) = product ( the Sorts of A * (the_arity_of (compsym (a,b,c)))) by PRALG_2:3
.= product ( the Sorts of A * <*(homsym (b,c)),(homsym (a,b))*>) by Def3
.= product <*( the Sorts of A . (homsym (b,c))),( the Sorts of A . (homsym (a,b)))*> by A2, FINSEQ_2:125
.= 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:3
.= the Sorts of A . (homsym (a,c)) by Def3
.= Hom (a,c) by A1 ; :: thesis: verum