theorem :: FINSOP_1:20

for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F = 1 holds
g "**" F = F . 1 by Lm11;