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, Th67;
thus u . ((F * ((id D),u)) . (d1,d2)) = u . (F . (d1,(u . d2))) by Th87
.= F . ((u . d1),(u . (u . d2))) by A4, BINOP_1:def 12
.= F . ((u . d1),d2) by A1, A3, Th66
.= (F * (u,(id D))) . (d1,d2) by Th87 ; :: 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, Th66; :: thesis: verum