theorem Th3: :: HILB10_7:3

for D being non empty set
for A, M being BinOp of D st A is commutative & A is associative & A is having_a_unity & M is commutative & M is_distributive_wrt A & ( for d being Element of D holds M . ((the_unity_wrt A),d) = the_unity_wrt A ) holds
for X, Y being non empty finite set
for f being Function of X,D
for g being Function of Y,D
for a being Element of Fin X
for b being Element of Fin Y holds A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)))