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

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