for n being Nat
for f, g being FinSequence st n + 1 in dom f & g = f | (Seg n) holds
f | (Seg (n + 1)) = g ^ <*(f . (n + 1))*>