theorem Th44: :: FINSEQOP:44

for C, D being non empty set
for f being Function of C,D
for F being BinOp of D st F is having_a_unity holds
F [;] ((the_unity_wrt F),f) = f