for f, g being FinSequence of (TOP-REAL 2) st f is unfolded & g is unfolded & f /. (len f) = g /. 1 & (LSeg (f,((len f) -' 1))) /\ (LSeg (g,1)) = {(f /. (len f))} holds
f ^' g is unfolded