theorem :: FINSEQOP:46

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, G being BinOp of D st F is_distributive_wrt G holds
F [;] ((G . (d1,d2)),T) = G .: ((F [;] (d1,T)),(F [;] (d2,T)))