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