theorem Th29: :: MATRIX_3:29

for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of I,D
for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds
for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds
F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)