let D be non empty set ; :: thesis: for i being natural Number

for T being Tuple of i,D

for F being BinOp of D st F is having_a_unity holds

F [;] ((the_unity_wrt F),T) = T

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

for F being BinOp of D st F is having_a_unity holds

F [;] ((the_unity_wrt F),T) = T

let T be Tuple of i,D; :: thesis: for F being BinOp of D st F is having_a_unity holds

F [;] ((the_unity_wrt F),T) = T

let F be BinOp of D; :: thesis: ( F is having_a_unity implies F [;] ((the_unity_wrt F),T) = T )

assume A1: F is having_a_unity ; :: thesis: F [;] ((the_unity_wrt F),T) = T

for T being Tuple of i,D

for F being BinOp of D st F is having_a_unity holds

F [;] ((the_unity_wrt F),T) = T

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

for F being BinOp of D st F is having_a_unity holds

F [;] ((the_unity_wrt F),T) = T

let T be Tuple of i,D; :: thesis: for F being BinOp of D st F is having_a_unity holds

F [;] ((the_unity_wrt F),T) = T

let F be BinOp of D; :: thesis: ( F is having_a_unity implies F [;] ((the_unity_wrt F),T) = T )

assume A1: F is having_a_unity ; :: thesis: F [;] ((the_unity_wrt F),T) = T