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 . (the_unity_wrt G)),(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 . (the_unity_wrt G)),(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 . (the_unity_wrt G)),(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 . (the_unity_wrt G)),(id D)) = u
set o = the_unity_wrt G;
for d being Element of D holds (G [;] ((u . (the_unity_wrt G)),(id D))) . d = u . d

proof

let d be Element of D; :: thesis: (G [;] ((u . (the_unity_wrt G)),(id D))) . d = u . d
thus (G [;] ((u . (the_unity_wrt G)),(id D))) . d = G . ((u . (the_unity_wrt G)),((id D) . d)) by FUNCOP_1:53
.= G . ((u . (the_unity_wrt G)),d)
.= u . (G . ((the_unity_wrt G),d)) by A1, Th67
.= u . d by A2, SETWISEO:15 ; :: thesis: verum

end;

hence G [;] ((u . (the_unity_wrt G)),(id D)) = u by FUNCT_2:63; :: thesis: verum