theorem :: FINSEQOP:31

for D being non empty set
for d1, d2 being Element of D
for i being natural Number
for T being Tuple of i,D
for F being BinOp of D st F is associative holds
F [;] ((F . (d1,d2)),T) = F [;] (d1,(F [;] (d2,T)))