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:23
.= G . e,d by A2, A5, SETWISEO:23 ;
hence G . e,d = e by A1, A2, A3, A5, Th69; :: 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:23
.= G . d,e by A2, A5, SETWISEO:23 ;
hence G . d,e = e by A1, A2, A3, A5, Th69; :: thesis: verum