theorem Th31: :: FOMODEL0:31

for D being non empty set
for d being Element of D
for f being BinOp of D holds
( (MultPlace f) . <*d*> = d & ( for x being b₁ -valued FinSequence st not x is empty holds
(MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) )