theorem Th2: :: SETWOP_2:2

for C, D being non empty set
for c being Element of C
for B being Element of Fin C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & ( B <> {} or F is having_a_unity ) & not c in B holds
F $$ ((B \/ {.c.}),f) = F . ((F $$ (B,f)),(f . c))