for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F >= 1 holds
ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & g "**" F = f . (len F) ) by Def1;