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