theorem Th25: :: FINSEQOP:25

for C, D being non empty set
for d being Element of D
for f, f9 being Function of C,D
for F being BinOp of D st F is associative holds
(F [:] ((id D),d)) * (F .: (f,f9)) = F .: (f,((F [:] ((id D),d)) * f9))