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

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

hence
G [;] ((u . (the_unity_wrt G)),(id D)) = u
by FUNCT_2:63; :: thesis: verum
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;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