theorem Th36: :: FINSEQ_6:36

for x being set
for f1, f2 being FinSequence st not x in rng f1 holds
x .. ((f1 ^ <*x*>) ^ f2) = (len f1) + 1