let S be non empty non void ManySortedSign ; :: thesis: for a being SortSymbol of S
for o being OperSymbol of S st the_arity_of o = <*a*> holds
for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a)*>
let a be SortSymbol of S; :: thesis: for o being OperSymbol of S st the_arity_of o = <*a*> holds
for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a)*>
let o be OperSymbol of S; :: thesis: ( the_arity_of o = <*a*> implies for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a)*> )
assume A1: the_arity_of o = <*a*> ; :: thesis: for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a)*>
let A be MSAlgebra over S; :: thesis: Args (o,A) = product <*( the Sorts of A . a)*>
A2: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
thus Args (o,A) = product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3
.= product <*( the Sorts of A . a)*> by A1, A2, FINSEQ_2:34 ; :: thesis: verum