theorem :: FINSEQOP:68

for D being non empty set
for F, G being BinOp of D
for u being UnOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F & G is having_a_unity holds
G [;] ((u . (the_unity_wrt G)),(id D)) = u