let S be non empty non void ManySortedSign ; :: thesis:
let U0 be MSAlgebra of S; :: thesis:
let o be OperSymbol of S; :: thesis:
set So = the Sorts of U0;
set Ar = the Arity of S;
set Rs = the ResultSort of S;
set ar = the_arity_of o;
set AS = (the Sorts of U0 # ) * the Arity of S;
set RS = the Sorts of U0 * the ResultSort of S;
set X = the carrier' of S;
set Cr = the carrier of S;
A2: ( dom the Arity of S = the carrier' of S & rng the Arity of S c= the carrier of S * ) by FUNCT_2:def 1, RELSET_1:12;
then A3: dom ((the Sorts of U0 # ) * the Arity of S) = dom the Arity of S by PBOOLE:def 3;
thus Args o,U0 = ((the Sorts of U0 # ) * the Arity of S) . o by MSUALG_1:def 9
.= (the Sorts of U0 # ) . (the Arity of S . o) by A2, A3, FUNCT_1:22
.= (the Sorts of U0 # ) . (the_arity_of o) by MSUALG_1:def 6
.= product (the Sorts of U0 * (the_arity_of o)) by PBOOLE:def 19 ; :: thesis:
( rng (the_arity_of o) c= the carrier of S & dom the Sorts of U0 = the carrier of S ) by FINSEQ_1:def 4, PBOOLE:def 3;
hence dom (the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46; :: thesis:
A4: ( dom the ResultSort of S = the carrier' of S & rng the ResultSort of S c= the carrier of S ) by FUNCT_2:def 1, RELSET_1:12;
then A5: dom (the Sorts of U0 * the ResultSort of S) = dom the ResultSort of S by PBOOLE:def 3;
thus Result o,U0 = (the Sorts of U0 * the ResultSort of S) . o by MSUALG_1:def 10
.= the Sorts of U0 . (the ResultSort of S . o) by A4, A5, FUNCT_1:22
.= the Sorts of U0 . (the_result_sort_of o) by MSUALG_1:def 7 ; :: thesis: