theorem Th23: :: FILTER_1:23

for D1, D2 being non empty set
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )