for D being non empty set
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 .: ((i |-> (the_unity_wrt F)),T) = T & F .: (T,(i |-> (the_unity_wrt F))) = T )