let C be Category; 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; ( ( 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)
; 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; ( 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
; 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
; verum