for i being Nat
for x being FinSeqLen of i + 1 ex y being FinSeqLen of i ex a being object st x = y ^ <*a*> by Lm1;