theorem :: FINSEQOP:58

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