theorem :: SETWOP_2:17

for C, D being non empty set
for B being Element of Fin C
for F being BinOp of D
for u being UnOp of D
for f being Function of C,D st F is commutative & F is associative & F is having_a_unity & u . (the_unity_wrt F) = the_unity_wrt F & u is_distributive_wrt F holds
u . (F $$ (B,f)) = F $$ (B,(u * f)) by Th16;