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