let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S st the_arity_of o = {} holds
for A being MSAlgebra over S holds Args (o,A) = {{}}
let o be OperSymbol of S; :: thesis: ( the_arity_of o = {} implies for A being MSAlgebra over S holds Args (o,A) = {{}} )
assume A1: the_arity_of o = {} ; :: thesis: for A being MSAlgebra over S holds Args (o,A) = {{}}
let A be MSAlgebra over S; :: thesis: Args (o,A) = {{}}
thus Args (o,A) = product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3
.= {{}} by A1, CARD_3:10 ; :: thesis: verum