:: deftheorem Def7 defines MultPlace FOMODEL0:def 7 :
for D being non empty set
for f being BinOp of D
for x being FinSequence of D
for b₄ being Function holds
( b₄ = MultPlace (f,x) iff ( dom b₄ = NAT & b₄ . 0 = x . 1 & ( for n being Nat holds b₄ . (n + 1) = f . ((b₄ . n),(x . (n + 2))) ) ) );