theorem Th75: :: FINSEQOP:75

for C, D being non empty set
for e being Element of D
for f being Function of C,D
for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds
G [;] (e,f) = C --> e