theorem :: SETWOP_2:29

for D being non empty set
for F being BinOp of D
for u being UnOp of D
for p being FinSequence of D st F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F "**" p) = F "**" (u * p) by Th28;