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 A1: ( F is associative & F is having_a_unity & F is commutative & 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) )
then A2: u is_distributive_wrt F by Th67;
thus u . ((F * (id D),u) . d1,d2) = u . (F . d1,(u . d2)) by Th87
.= F . (u . d1),(u . (u . d2)) by A2, BINOP_1:def 12
.= F . (u . d1),d2 by A1, 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, Th66; :: thesis: verum