for D, I, J being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D st F is commutative & F is associative & G is commutative holds
for x being Element of I
for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))