let D be non empty set ; :: thesis: for e being Element of D
for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F holds
for d being Element of D holds
( G . (e,d) = e & G . (d,e) = e )
let e be Element of D; :: thesis: for F, G being BinOp of D st F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F holds
for d being Element of D holds
( G . (e,d) = e & G . (d,e) = e )
let F, G be BinOp of D; :: thesis: ( F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F implies for d being Element of D holds
( G . (e,d) = e & G . (d,e) = e ) )
assume that
A1: F is associative and
A2: F is having_a_unity and
A3: F is having_an_inverseOp and
A4: G is_distributive_wrt F and
A5: e = the_unity_wrt F ; :: thesis: for d being Element of D holds
( G . (e,d) = e & G . (d,e) = e )
let d be Element of D; :: thesis: ( G . (e,d) = e & G . (d,e) = e )
set ed = G . (e,d);
F . ((G . (e,d)),(G . (e,d))) = G . ((F . (e,e)),d) by A4, BINOP_1:11
.= G . (e,d) by A2, A5, SETWISEO:15 ;
hence G . (e,d) = e by A1, A2, A3, A5, Th65; :: thesis: G . (d,e) = e
set de = G . (d,e);
F . ((G . (d,e)),(G . (d,e))) = G . (d,(F . (e,e))) by A4, BINOP_1:11
.= G . (d,e) by A2, A5, SETWISEO:15 ;
hence G . (d,e) = e by A1, A2, A3, A5, Th65; :: thesis: verum