theorem Th22: :: FILTER_1:22

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