theorem :: FINSEQOP:54

for D being non empty set
for d being Element of D
for F, G being BinOp of D
for u being UnOp of D st G is_distributive_wrt F & u = G [;] (d,(id D)) holds
u is_distributive_wrt F