let D be non empty set ; :: thesis: for e being Element of D

for i being natural Number

for T being Tuple of i,D

for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds

G [;] (e,T) = i |-> e

let e be Element of D; :: thesis: for i being natural Number

for T being Tuple of i,D

for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds

G [;] (e,T) = i |-> e

let i be natural Number ; :: thesis: for T being Tuple of i,D

for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds

G [;] (e,T) = i |-> e

let T be Tuple of i,D; :: thesis: for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds

G [;] (e,T) = i |-> e

let F, G be BinOp of D; :: thesis: ( F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F implies G [;] (e,T) = i |-> e )

assume A1: ( F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F ) ; :: thesis: G [;] (e,T) = i |-> e

for i being natural Number

for T being Tuple of i,D

for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds

G [;] (e,T) = i |-> e

let e be Element of D; :: thesis: for i being natural Number

for T being Tuple of i,D

for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds

G [;] (e,T) = i |-> e

let i be natural Number ; :: thesis: for T being Tuple of i,D

for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds

G [;] (e,T) = i |-> e

let T be Tuple of i,D; :: thesis: for F, G being BinOp of D st F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F holds

G [;] (e,T) = i |-> e

let F, G be BinOp of D; :: thesis: ( F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F implies G [;] (e,T) = i |-> e )

assume A1: ( F is associative & F is having_a_unity & e = the_unity_wrt F & F is having_an_inverseOp & G is_distributive_wrt F ) ; :: thesis: G [;] (e,T) = i |-> e