theorem Th82: :: FINSEQOP:83

for C, D being non empty set
for f, f9 being Function of C,D
for F being BinOp of D
for u being UnOp of D holds (F * ((id D),u)) .: (f,f9) = F .: (f,(u * f9))