let S be non empty non void ManySortedSign ; 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; 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; ( 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*>
; 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; 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
; verum