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:23
.= G . (the_unity_wrt F),d2 by A1, A2, Th63
.= the_unity_wrt F by A1, A3, Th70 ;
hence u . (G . d1,d2) = G . (u . d1),d2 by A1, A2, Th64; :: 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:23
.= G . d1,(the_unity_wrt F) by A1, A2, Th63
.= the_unity_wrt F by A1, A3, Th70 ;
hence u . (G . d1,d2) = G . d1,(u . d2) by A1, A2, Th64; :: thesis: verum