theorem Th4: :: MONOID_1:4

for A being set
for D being non empty set
for o being BinOp of D
for f, g, h being Function of A,D st o is associative holds
o .: ((o .: (f,g)),h) = o .: (f,(o .: (g,h)))