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
for X being Element of Fin I
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))