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 [:] (T,(the_unity_wrt F)) = 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 [:] (T,(the_unity_wrt F)) = T

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

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

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

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

for T being Tuple of i,D

for F being BinOp of D st F is having_a_unity holds

F [:] (T,(the_unity_wrt F)) = 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 [:] (T,(the_unity_wrt F)) = T

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

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

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

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