let S be non empty non void ManySortedSign ; for U0 being MSAlgebra over S
for o being OperSymbol of S holds
( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
let U0 be MSAlgebra over S; for o being OperSymbol of S holds
( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
let o be OperSymbol of S; ( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
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 2;
thus Args (o,U0) =
(( the Sorts of U0 #) * the Arity of S) . o
by MSUALG_1:def 4
.=
( the Sorts of U0 #) . ( the Arity of S . o)
by A1, A2, FUNCT_1:12
.=
( the Sorts of U0 #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product ( the Sorts of U0 * (the_arity_of o))
by FINSEQ_2:def 5
; ( dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
( 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 2;
hence
dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:27; Result (o,U0) = the Sorts of U0 . (the_result_sort_of o)
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 2;
thus Result (o,U0) =
( the Sorts of U0 * the ResultSort of S) . o
by MSUALG_1:def 5
.=
the Sorts of U0 . ( the ResultSort of S . o)
by A3, A4, FUNCT_1:12
.=
the Sorts of U0 . (the_result_sort_of o)
by MSUALG_1:def 2
; verum