theorem :: FINSEQOP:26

for D being non empty set
for d being Element of D
for i being natural Number
for T1, T2 being Tuple of i,D
for F being BinOp of D st F is associative holds
(F [;] (d,(id D))) * (F .: (T1,T2)) = F .: (((F [;] (d,(id D))) * T1),T2)