let D be non empty set ; :: thesis: 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 . ()),(id D)) = u

let F, G be BinOp of D; :: thesis: 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 . ()),(id D)) = u

let u be UnOp of D; :: thesis: ( 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 implies G [;] ((u . ()),(id D)) = u )
assume that
A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F ) and
A2: G is having_a_unity ; :: thesis: G [;] ((u . ()),(id D)) = u
set o = the_unity_wrt G;
for d being Element of D holds (G [;] ((u . ()),(id D))) . d = u . d
proof
let d be Element of D; :: thesis: (G [;] ((u . ()),(id D))) . d = u . d
thus (G [;] ((u . ()),(id D))) . d = G . ((u . ()),((id D) . d)) by FUNCOP_1:53
.= G . ((u . ()),d)
.= u . (G . ((),d)) by
.= u . d by ; :: thesis: verum
end;
hence G [;] ((u . ()),(id D)) = u by FUNCT_2:63; :: thesis: verum