let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of S
for o being OperSymbol of S st the_arity_of o = {} holds
Args o,U0 = {{} }
let U0 be MSAlgebra of 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 Th10
.= {{} } by A1, CARD_3:19 ; :: thesis: verum