theorem :: FOMODEL0:13

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 non empty FinSequence of D holds (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) ) by Lm15;