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;
A1: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then A2: dom ((the Sorts of U0 # ) * the Arity of S) = dom the Arity of S by PARTFUN1:def 4;
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 A1, A2, 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, PARTFUN1:def 4;
hence dom (the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46; :: thesis:
A3: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then A4: dom (the Sorts of U0 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def 4;
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 A3, A4, FUNCT_1:22
.= the Sorts of U0 . (the_result_sort_of o) by MSUALG_1:def 7 ; :: thesis: