let S be non empty non void ManySortedSign ; :: thesis: for a, b being SortSymbol of S
for o being OperSymbol of S st the_arity_of o = <*a,b*> holds
for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b)*>
let a, b be SortSymbol of S; :: thesis: for o being OperSymbol of S st the_arity_of o = <*a,b*> holds
for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b)*>
let o be OperSymbol of S; :: thesis: ( the_arity_of o = <*a,b*> implies for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b)*> )
assume A1: the_arity_of o = <*a,b*> ; :: thesis: for A being MSAlgebra over S holds Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b)*>
let A be MSAlgebra over S; :: thesis: Args (o,A) = product <*( the Sorts of A . a),( the Sorts of A . b)*>
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),( the Sorts of A . b)*> by A1, A2, FINSEQ_2:125 ; :: thesis: verum