let D be non empty set ; :: thesis: for d1, d2 being Element of D

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 holds

( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )

let d1, d2 be Element of D; :: 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 holds

( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )

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 holds

( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )

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 implies ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) ) )

assume that

A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp ) and

A2: u = the_inverseOp_wrt F and

A3: G is_distributive_wrt F ; :: thesis: ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )

set e = the_unity_wrt F;

F . ((G . (d1,d2)),(G . ((u . d1),d2))) = G . ((F . (d1,(u . d1))),d2) by A3, BINOP_1:11

.= G . ((the_unity_wrt F),d2) by A1, A2, Th59

.= the_unity_wrt F by A1, A3, Th66 ;

hence u . (G . (d1,d2)) = G . ((u . d1),d2) by A1, A2, Th60; :: thesis: u . (G . (d1,d2)) = G . (d1,(u . d2))

F . ((G . (d1,d2)),(G . (d1,(u . d2)))) = G . (d1,(F . (d2,(u . d2)))) by A3, BINOP_1:11

.= G . (d1,(the_unity_wrt F)) by A1, A2, Th59

.= the_unity_wrt F by A1, A3, Th66 ;

hence u . (G . (d1,d2)) = G . (d1,(u . d2)) by A1, A2, Th60; :: thesis: verum

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 holds

( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )

let d1, d2 be Element of D; :: 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 holds

( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )

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 holds

( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )

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 implies ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) ) )

assume that

A1: ( F is having_a_unity & F is associative & F is having_an_inverseOp ) and

A2: u = the_inverseOp_wrt F and

A3: G is_distributive_wrt F ; :: thesis: ( u . (G . (d1,d2)) = G . ((u . d1),d2) & u . (G . (d1,d2)) = G . (d1,(u . d2)) )

set e = the_unity_wrt F;

F . ((G . (d1,d2)),(G . ((u . d1),d2))) = G . ((F . (d1,(u . d1))),d2) by A3, BINOP_1:11

.= G . ((the_unity_wrt F),d2) by A1, A2, Th59

.= the_unity_wrt F by A1, A3, Th66 ;

hence u . (G . (d1,d2)) = G . ((u . d1),d2) by A1, A2, Th60; :: thesis: u . (G . (d1,d2)) = G . (d1,(u . d2))

F . ((G . (d1,d2)),(G . (d1,(u . d2)))) = G . (d1,(F . (d2,(u . d2)))) by A3, BINOP_1:11

.= G . (d1,(the_unity_wrt F)) by A1, A2, Th59

.= the_unity_wrt F by A1, A3, Th66 ;

hence u . (G . (d1,d2)) = G . (d1,(u . d2)) by A1, A2, Th60; :: thesis: verum