:: deftheorem Def9 defines MultPlace FOMODEL0:def 9 :
for D being non empty set
for f being BinOp of D
for b₃ being Function of ((D *) \ {{}}),D holds
( b₃ = MultPlace f iff for x being Element of (D *) \ {{}} holds b₃ . x = (MultPlace (f,x)) . ((len x) - 1) );