theorem Th24: :: FINSEQOP:24

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 [;] (d,(id D))) * (F .: (f,f9)) = F .: (((F [;] (d,(id D))) * f),f9)