let D be non empty set ; :: thesis: for d1, d2 being Element of D
for F being BinOp of D
for u being UnOp of D st F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = the_inverseOp_wrt F holds
( u . ((F * ((id D),u)) . (d1,d2)) = (F * (u,(id D))) . (d1,d2) & (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) )
let d1, d2 be Element of D; :: thesis: for F being BinOp of D
for u being UnOp of D st F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = the_inverseOp_wrt F holds
( u . ((F * ((id D),u)) . (d1,d2)) = (F * (u,(id D))) . (d1,d2) & (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) )
let F be BinOp of D; :: thesis: for u being UnOp of D st F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = the_inverseOp_wrt F holds
( u . ((F * ((id D),u)) . (d1,d2)) = (F * (u,(id D))) . (d1,d2) & (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) )
let u be UnOp of D; :: thesis: ( F is associative & F is having_a_unity & F is commutative & F is having_an_inverseOp & u = the_inverseOp_wrt F implies ( u . ((F * ((id D),u)) . (d1,d2)) = (F * (u,(id D))) . (d1,d2) & (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) ) )
assume that
A1: ( F is associative & F is having_a_unity ) and
A2: F is commutative and
A3: ( F is having_an_inverseOp & u = the_inverseOp_wrt F ) ; :: thesis: ( u . ((F * ((id D),u)) . (d1,d2)) = (F * (u,(id D))) . (d1,d2) & (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) )
A4: u is_distributive_wrt F by A1, A2, A3, Th63;
thus u . ((F * ((id D),u)) . (d1,d2)) = u . (F . (d1,(u . d2))) by Th81
.= F . ((u . d1),(u . (u . d2))) by A4
.= F . ((u . d1),d2) by A1, A3, Th62
.= (F * (u,(id D))) . (d1,d2) by Th81 ; :: thesis: (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2))
hence (F * ((id D),u)) . (d1,d2) = u . ((F * (u,(id D))) . (d1,d2)) by A1, A3, Th62; :: thesis: verum