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

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