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:66
.= G . (u . (the_unity_wrt G)),d by FUNCT_1:35
.= u . (G . (the_unity_wrt G),d) by A1, Th71
.= u . d by A2, SETWISEO:23 ; :: thesis: verum

end;

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