theorem :: FACIRC_2:34

for i being Nat
for x being nonpair-yielding FinSeqLen of i + 1 ex y being nonpair-yielding FinSeqLen of i ex a being non pair set st x = y ^ <*a*> by Lm2;